(*
  Author: Fred Kurz
*)
theory List_Supplement
imports Main
begin

lemma list_foot: 
  assumes "l ≠ []" 
  obtains y ys where "l = ys @ [y]"
proof -
  {
    assume a: "l ≠ []"
    have "∃y ys. l = ys @ [y]" 
      using a 
      proof (induction l)
        case (Cons a l)
        then show ?case 
          proof (cases "l = []")
            case True
            have "[] @ [a] = a # l" 
              using True
              by simp
            thus ?thesis 
              using Cons.prems(1)
              by simp
          next
            case False
            thm Cons
            then obtain y ys where "l = ys @ [y]" 
              using Cons.IH
              by blast
            then have "a # l = a # ys @ [y]" 
              by blast
            thus ?thesis
              by fastforce
          qed
      qed simp
  }
  thus ?thesis 
    using assms that 
    by blast
qed

lemma list_ex_intersection: "list_ex (λv. list_ex ((=) v) ys) xs ⟷ set xs ∩ set ys ≠ {}"
proof -
  {
    assume "list_ex (λv. list_ex ((=) v) ys) xs"
    then have "∃v ∈ set xs. list_ex ((=) v) ys" 
      using list_ex_iff
      by fast
    moreover have "∀v. list_ex ((=) v) ys = (∃v' ∈ set ys. v = v')" 
      using list_ex_iff
      by blast
    ultimately have "∃v ∈ set xs. (∃v' ∈ set ys. v = v')"
      by blast
    then obtain v v' where "v ∈ set xs" and "v' ∈ set ys" and "v = v'"
      by blast
    then have "set xs ∩ set ys ≠ {}"
      by blast
  } moreover {
    assume  "set xs ∩ set ys ≠ {}"
    then obtain v v' where "v ∈ set xs" and "v' ∈ set ys" and "v = v'"
      by blast
    then have "list_ex (λv. ∃v' ∈ set ys. v = v') xs" 
      using list_ex_iff 
      by fast
    moreover have "∀v. (∃v' ∈ set ys. v = v') = list_ex ((=) v) ys" 
      using list_ex_iff
      by blast
    ultimately have "list_ex (λv. list_ex ((=) v) ys) xs" 
      by force
  } ultimately show ?thesis
    by blast
qed

lemma length_map_upt: "length (map f [a..<b]) = b - a" 
proof -
  have "length [a..<b] = b - a" 
    using length_upt
    by blast
  moreover have "length (map f [a..<b]) = length [a..<b]"
    by simp
  ultimately show ?thesis
    by argo
qed

lemma not_list_ex_equals_list_all_not: "(¬list_ex P xs) = list_all (λx. ¬P x) xs" 
proof -
  have "(¬list_ex P xs) = (¬Bex (set xs) P)"
    using list_ex_iff 
    by blast
  also have "… = Ball (set xs) (λx. ¬P x)"
    by blast 
  finally show ?thesis
    by (simp add: Ball_set_list_all)
qed

lemma element_of_subseqs_then_subset:
  assumes "l ∈ set (subseqs l')" 
  shows"set l ⊆ set l'" 
  using assms
proof (induction l' arbitrary: l)
  case (Cons x l')
  have "set (subseqs (x # l')) = (Cons x) ` set (subseqs l') ∪ set (subseqs l')"
    unfolding subseqs.simps(2) Let_def set_map set_append..
  then consider (A) "l ∈ (Cons x) ` set (subseqs l')"
    | (B) "l ∈ set (subseqs l')" 
    using Cons.prems
    by blast
  thus ?case 
    proof (cases)
      case A
      then obtain l'' where "l'' ∈ set (subseqs l')" and "l = x # l''" 
        by blast
      moreover have "set l'' ⊆ set l'" 
        using Cons.IH[of l'', OF calculation(1)].
      ultimately show ?thesis 
        by auto
    next
      case B
      then show ?thesis 
        using Cons.IH
        by auto
    qed
qed simp

(* TODO rewrite using list comprehension ‹embed xs = [[x]. x ← xs]› *)
text ‹ Embed a list into a list of singleton lists. ›
primrec embed :: "'a list ⇒ 'a list list" 
  where "embed [] = []" 
  | "embed (x # xs) = [x] # embed xs"

lemma set_of_embed_is: "set (embed xs) = { [x] | x. x ∈ set xs }" 
  by (induction xs; force+)

lemma concat_is_inverse_of_embed:
  "concat (embed xs) = xs"
  by (induction xs; simp)

lemma embed_append[simp]: "embed (xs @ ys) = embed xs @ embed ys"
proof (induction xs)
  case (Cons x xs)
  have "embed (x # xs @ ys) = [x] # embed (xs @ ys)" 
    try0
    by simp
  also have "… = [x] # (embed xs @ embed ys)" 
    using Cons.IH 
    by simp
  finally show ?case 
    by fastforce
qed simp

end

(*
  Author: Fred Kurz
*)
theory Map_Supplement
imports Main
begin

lemma map_of_defined_if_constructed_from_list_of_constant_assignments:
  "l = map (λx. (x, a)) xs ⟹ ∀x ∈ set xs. (map_of l) x = Some a" 
proof (induction xs arbitrary: l)
  case (Cons x xs)
  let ?l' = "map (λv. (v, a)) xs"
  from Cons.prems(1) have "l = (x, a) # map (λv. (v, a)) xs" 
    by force
  moreover have "∀v ∈ set xs. (map_of ?l') v = Some a" 
    using Cons.IH[where l="?l'"]
    by blast
  ultimately show ?case
    by auto
qed auto

― ‹ NOTE Function graph is the set of pairs (x, f x) for a (total) function f. ›
― ‹ TODO Remove the first premise (follows from the second). ›
lemma map_of_from_function_graph_is_some_if:
  fixes f :: "'a ⇒ 'b"
  assumes "set xs ≠ {}"
   and "x ∈ set xs"
  shows "(map_of (map (λx. (x, f x)) xs)) x = Some (f x)" 
  using assms 
proof (induction xs arbitrary: f x)
  ― ‹ NOTE Base case follows trivially from violation of assumption ‹set xs ≠ {}›. ›
  case (Cons a xs)
    thm Cons
    let ?m = "map_of (map (λx. (x, f x)) xs)" 
    have a: "map_of (map (λx. (x, f x)) (Cons a xs)) = ?m(a ↦ f a)" 
      unfolding map_of_def
      by simp
    thus ?case 
      proof(cases "x = a")
        case False
        thus ?thesis 
        proof (cases "set xs = {}")
            ― ‹ NOTE Follows from contradiction (‹x ∈ set (Cons a xs) ∧ set xs = {} ∧ x ≠ a ≡ ⊥›)›
            case True
            thus ?thesis 
              using Cons.prems(2)
              by fastforce
          next
            case False
            then have "x ∈ set xs" 
              using ‹x ≠ a› Cons.prems(2)
              by fastforce
            moreover have "map_of (map (λx. (x, f x)) (Cons a xs)) x = ?m x"
              using ‹x ≠ a›
              by fastforce
            ultimately show ?thesis 
              using Cons.IH[OF False]
              by presburger
          qed 
      qed force
    qed blast

lemma foldl_map_append_is_some_if:
  assumes "b x = Some y ∨ (∃m ∈ set ms. m x = Some y)" 
    and "∀m' ∈ set ms. m' x = Some y ∨ m' x = None"
  shows "foldl (++) b ms x = Some y" 
using assms
proof (induction ms arbitrary: b)
  ― ‹ NOTE Induction base case violates first assumption (we have at least one element in ms 
    and hence ‹ms ≠ []›). ›
  case (Cons a ms)
  consider (b_is_some_y) "b x = Some y" 
    | (m_is_some_y) "∃m ∈ set (a # ms). m x = Some y" 
    using Cons.prems(1)
    by blast
  hence "(b ++ a) x = Some y ∨ (∃m∈set ms. m x = Some y)"
    proof (cases)
      case b_is_some_y
      moreover have "a x = Some y ∨ a x = None" 
        using Cons.prems(2)
        by simp
      ultimately show ?thesis 
        using map_add_Some_iff[of b a x y]
        by blast
    next
      case m_is_some_y
      then show ?thesis 
        proof (cases "a x = Some y")
          case False 
          then obtain m where "m ∈ set ms" and "m x = Some y" 
            using m_is_some_y try0
            by auto
          thus ?thesis
            by blast
        qed simp
    qed
  moreover have "∀m' ∈ set ms. m' x = Some y ∨ m' x = None"  
    using Cons.prems(2)
    by fastforce
  ultimately show ?case using Cons.IH[where b="b ++ a"]
    by simp
qed auto

(* TODO "∀(v, a) ∈ set l. ∀(v', a') ∈ set l. v ≠ v' ∨ a = a'" ↝
  "∀(v', a') ∈ set l. v ≠ v' ∨ a = a'" (this is too strong; we only consider (v, a), i.e. fixed v)
*)
(* TODO isn't this the same as map_of_is_SomeI? *)
lemma map_of_constant_assignments_defined_if:
  assumes "∀(v, a) ∈ set l. ∀(v', a') ∈ set l. v ≠ v' ∨ a = a'"
    and "(v, a) ∈ set l" 
  shows "map_of l v = Some a" 
  using assms
proof (induction l)
  case (Cons x l)
  thm Cons
  then show ?case 
    proof (cases "x = (v, a)")
      case False
      have v_a_in_l: "(v, a) ∈ set l" 
        using Cons.prems(2) False
        by fastforce
      {
        have "∀(v, a) ∈ set l. ∀(v', a') ∈ set l. v ≠ v' ∨ a = a'"
          using Cons.prems(1)
          by auto 
        hence "map_of l v = Some a"
          using Cons.IH v_a_in_l
          by linarith
      } note ih = this
      {
        have "x ∈ set (x # l)" 
          by auto
        hence "fst x ≠ v ∨ snd x = a" 
          using Cons.prems(1) v_a_in_l
          by fastforce
      } note nb = this
      ― ‹ NOTE If @{text "fst x = v"} then @{text "snd x = a"} by fact @{text "nb"}; moreover if 
        on the other hand @{text "fst x ≠ v"}, then the proposition follows from the induction 
        hypothesis since @{text "map_of (x # l) v = map_of l v"} in that case. ›
      thus ?thesis
        using ih nb
        by (cases "fst x = v") fastforce+
    qed simp
qed fastforce

end

(*
  Author: Fred Kurz
*)
theory CNF_Supplement
  imports "Propositional_Proof_Systems.CNF_Formulas_Sema"
begin

(* TODO fix warnings *)

fun is_literal_formula 
  where "is_literal_formula (Atom _) = True"
  | "is_literal_formula (❙¬(Atom _)) = True" 
  | "is_literal_formula _ = False" 

fun literal_formula_to_literal :: "'a formula ⇒ 'a literal"
  where "literal_formula_to_literal (Atom a) = a⇧+"
  | "literal_formula_to_literal (❙¬(Atom a)) = a¯" 

lemma is_literal_formula_then_cnf_is_singleton_clause:
  assumes "is_literal_formula f"
  obtains C where "cnf f = { C }" 
proof -
  consider (f_is_positive_literal) "∃a. f = Atom a" 
    | (f_is_negative_literal) "∃a. f = ❙¬(Atom a)"
    using assms is_literal_formula.elims(2)[of f]
    by meson 
  then have "∃C. cnf f = { C }"
    proof (cases)
      case f_is_positive_literal
      then obtain a where "f = Atom a" 
        by force
      then have "cnf f = {{ a⇧+ }}"
        by force
      thus ?thesis
        by simp
    next
      case f_is_negative_literal
      then obtain a where "f = ❙¬(Atom a)" 
        by force
      then have "cnf f = {{ a¯ }}"
        by force
      thus ?thesis
        by simp
    qed
  thus ?thesis 
    using that
    by presburger 
qed

lemma literal_formula_to_literal_is_inverse_of_form_of_lit: 
  "literal_formula_to_literal (form_of_lit L) = L"
  by (cases L, simp+)

lemma is_nnf_cnf: 
  assumes "is_cnf F" 
    shows "is_nnf F" 
  using assms 
proof (induction F)
  case (Or F1 F2)
  have "is_disj (F1 ❙∨ F2)"
    using Or.prems is_cnf.simps(5)
    by simp
  thus ?case 
    using disj_is_nnf 
    by blast
qed simp+

lemma cnf_of_literal_formula:
  assumes "is_literal_formula f" 
  shows "cnf f = {{ literal_formula_to_literal f }}"
proof -
  consider (f_is_positive_literal) "∃a. f = Atom a"
    | (f_is_negative_literal) "∃a. f = (❙¬(Atom a))"
    using assms is_literal_formula.elims(2)[of f "∃a. f = Atom a"]
       is_literal_formula.elims(2)[of f "∃a. f = (❙¬(Atom a))"]
    by blast
  thus ?thesis 
    by(cases, force+)
qed

lemma is_cnf_foldr_and_if: 
  assumes "∀f ∈ set fs. is_cnf f"
  shows "is_cnf (foldr (❙∧) fs (❙¬⊥))" 
  using assms
proof (induction fs)
  case (Cons f fs)
  have "foldr (❙∧) (f # fs) (❙¬⊥) = f ❙∧ (foldr (❙∧) fs (❙¬⊥))" 
    by simp
  moreover {
    have "∀f ∈ set fs. is_cnf f" 
      using Cons.prems
      by force
    hence "is_cnf (foldr (❙∧) fs (❙¬⊥))" 
      using Cons.IH
      by blast
  }
  moreover have "is_cnf f" 
    using Cons.prems
    by simp
  ultimately show ?case
    by simp
qed simp

end

(*
  Author: Fred Kurz
*)
theory CNF_Semantics_Supplement
  imports "Propositional_Proof_Systems.CNF_Formulas_Sema" "CNF_Supplement"
begin

lemma not_model_if_exists_unmodeled_singleton_clause:
  assumes "is_cnf F"
    and "{L} ∈ cnf F"
    and "¬lit_semantics ν L" 
  shows "¬ν ⊨ F" 
proof (rule ccontr)
  assume "¬¬ν ⊨ F"  
  then have a: "ν ⊨ F"
    by blast
  moreover have "is_nnf F" 
    using is_nnf_cnf[OF assms(1)]
    by simp 
  moreover {
    let ?C = "{L}" 
    have "¬(∃L'. L' ∈ ?C ∧ lit_semantics ν L')" 
      using assms(3)
      by fast
    then have "¬(∀C ∈ cnf F. ∃L. L ∈ C ∧ lit_semantics ν L)"
      using assms(2)
      by blast
    hence "¬cnf_semantics ν (cnf F)" 
      unfolding cnf_semantics_def clause_semantics_def
      by fast
  }
  ultimately have "¬ ν ⊨ F" 
    using cnf_semantics
    by blast
  thus False 
    using a 
    by blast
qed

― ‹ NOTE This follows by contraposition from the previous lemma 
‹not_model_if_exists_unmodeled_singleton_clause›. ›
corollary model_then_all_singleton_clauses_modelled:
  assumes "is_cnf F"
    and "{L} ∈ cnf F"
    and "ν ⊨ F" 
  shows "lit_semantics ν L" 
  using not_model_if_exists_unmodeled_singleton_clause[OF assms(1, 2)] assms(3)
  by blast

― ‹ NOTE This is essentially the ‹⇒› direction of the compactness theorem when treating CNFs as sets
of formulas (sets of disjunctions in this case). ›
lemma model_for_cnf_is_model_of_all_subsets:
  assumes "cnf_semantics ν ℱ"
    and "ℱ' ⊆ ℱ" 
  shows "cnf_semantics ν ℱ'" 
proof -
  {
    fix C
    assume "C ∈ ℱ'"
    then have "C ∈ ℱ" 
      using assms(2)
      by blast
    then have "clause_semantics ν C" 
      using assms(1)
      unfolding cnf_semantics_def
      by blast
  }
  thus ?thesis 
    unfolding cnf_semantics_def
    by blast
qed

lemma cnf_semantics_monotonous_in_cnf_subsets_if:
  assumes "𝒜 ⊨ Φ" 
    and "is_cnf Φ" 
    and "cnf Φ' ⊆ cnf Φ" 
  shows "cnf_semantics 𝒜 (cnf Φ')"
proof -
  {
    have "is_nnf Φ"
      using is_nnf_cnf[OF assms(2)].
    hence "cnf_semantics 𝒜 (cnf Φ)" 
      using cnf_semantics assms(1)
      by blast
  }
  thus ?thesis 
    using model_for_cnf_is_model_of_all_subsets[OF _ assms(3)]
    by simp
qed

corollary modelling_relation_monotonous_in_cnf_subsets_if:
  assumes "𝒜 ⊨ Φ" 
    and "is_cnf Φ" 
    and "is_cnf Φ'"
    and "cnf Φ' ⊆ cnf Φ" 
  shows "𝒜 ⊨ Φ'"
proof -
  have "cnf_semantics 𝒜 (cnf Φ')" 
    using cnf_semantics_monotonous_in_cnf_subsets_if[OF assms(1, 2, 4)].
  thus ?thesis
    using cnf_semantics is_nnf_cnf[OF assms(3)]
    by blast  
qed

― ‹ NOTE Show that any clause ‹C› containing a subset ‹C› for which all literals
  ‹L› evaluate to ‹False› for the given valuation ‹𝒜›, then the clause
  semantics evaluation can be reduced to the set ‹C - C'› where all literals of 
  ‹C'› have been removed. ›
lemma lit_semantics_reducible_to_subset_if:
  assumes "C' ⊆ C"
    and "∀L ∈ C'. ¬lit_semantics 𝒜 L"
  shows "clause_semantics 𝒜 C = clause_semantics 𝒜 (C - C')"
  unfolding clause_semantics_def
  using assms
  by fast

end

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory State_Variable_Representation
  imports Main "Propositional_Proof_Systems.Formulas" "Propositional_Proof_Systems.Sema" 
    "Propositional_Proof_Systems.CNF"
begin
section "State-Variable Representation"

text ‹ Moving on to the Isabelle implementation of state-variable representation, we
first add a more concrete representation of states using Isabelle maps. To this end, we add a 
type synonym \isaname{state} for maps of variables to values. 
Since maps can be conveniently constructed from lists of 
assignments---i.e. pairs ‹(v, a) :: 'variable × 'domain›---we also add a corresponding type 
synonym \isaname{assignment}. ›

type_synonym ('variable, 'domain) state = "'variable ⇀ 'domain"

type_synonym ('variable, 'domain) assignment = "'variable × 'domain"

text ‹ Effects and effect condition (see \autoref{sub:state-variable-representation}) are 
implemented in a straight forward manner using a datatype with constructors for each effect type.›

type_synonym ('variable, 'domain) Effect = "('variable × 'domain) list"

end

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory STRIPS_Representation
  imports State_Variable_Representation
begin

section "STRIPS Representation"

(*<*)
type_synonym  ('variable) strips_state = "('variable, bool) state"
(*>*)
text ‹ We start by declaring a \isakeyword{record} for STRIPS operators.
This which allows us to define a data type and automatically generated selector operations. 
\footnote{For the full reference on records see \cite[11.6, pp.260-265]{wenzel--2018}} 

The record specification given below closely resembles the canonical representation of
STRIPS operators with fields corresponding to precondition, add effects as well as delete effects.›

record  ('variable) strips_operator = 
  precondition_of :: "'variable list" 
  add_effects_of :: "'variable list" 
  delete_effects_of :: "'variable list" 

― ‹ This constructor function is sometimes a more descriptive and replacement for the record 
syntax and can moreover be helpful if the record syntax leads to type ambiguity.›
abbreviation  operator_for
  :: "'variable list ⇒ 'variable list ⇒ 'variable list ⇒ 'variable strips_operator"
  where "operator_for pre add delete ≡ ⦇ 
    precondition_of = pre
    , add_effects_of = add
    , delete_effects_of = delete ⦈" 

definition  to_precondition
  :: "'variable strips_operator ⇒ ('variable, bool) assignment list"
  where "to_precondition op ≡ map (λv. (v, True)) (precondition_of op)" 

definition  to_effect
  :: "'variable strips_operator ⇒ ('variable, bool) Effect" 
  where "to_effect op =  [(v⇩a, True). v⇩a ← add_effects_of op] @ [(v⇩d, False). v⇩d ← delete_effects_of op]"

text ‹ Similar to the operator definition, we use a record to represent STRIPS problems and specify
fields for the variables, operators, as well as the initial and goal state. ›

record  ('variable) strips_problem =
  variables_of :: "'variable list" ("(_⇩𝒱)" [1000] 999)
  operators_of :: "'variable strips_operator list" ("(_⇩𝒪)" [1000] 999)
  initial_of :: "'variable strips_state" ("(_⇩I)" [1000] 999)
  goal_of :: "'variable strips_state" ("(_⇩G)" [1000] 999)

value  "stop" (* Tell document preparation to stop collecting for the last tag *)
(*<*)
― ‹ This constructor function is sometimes a more descriptive and replacement for the record 
syntax and can moreover be helpful if the record syntax leads to type ambiguity.›
(* TODO change identifier gs ~> G *)
abbreviation problem_for 
  :: "'variable list 
  ⇒ 'variable strips_operator list 
  ⇒ 'variable strips_state 
  ⇒ 'variable strips_state
  ⇒ ('variable) strips_problem"
  where "problem_for vs ops I gs ≡ ⦇ 
    variables_of = vs
    , operators_of = ops
    , initial_of = I
    , goal_of = gs ⦈" 

type_synonym ('variable) strips_plan = "'variable strips_operator list"

type_synonym ('variable) strips_parallel_plan = "'variable strips_operator list list"

definition is_valid_operator_strips
  :: "'variable strips_problem ⇒ 'variable strips_operator ⇒ bool"
  where "is_valid_operator_strips Π op ≡ let 
      vs = variables_of Π 
      ; pre = precondition_of op
      ; add = add_effects_of op
      ; del = delete_effects_of op
    in list_all (λv. ListMem v vs) pre 
    ∧ list_all (λv. ListMem v vs) add
    ∧ list_all (λv. ListMem v vs) del
    ∧ list_all (λv. ¬ListMem v del) add
    ∧ list_all (λv. ¬ListMem v add) del"

definition "is_valid_problem_strips Π
  ≡ let ops = operators_of Π
      ; vs = variables_of Π
      ; I = initial_of Π
      ; G = goal_of Π
    in  list_all (is_valid_operator_strips Π) ops 
    ∧ (∀v. I v ≠ None ⟷ ListMem v vs) 
    ∧ (∀v. G v ≠ None ⟶ ListMem v vs)"

definition is_operator_applicable_in
  :: "'variable strips_state ⇒ 'variable strips_operator ⇒ bool"
  where "is_operator_applicable_in s op ≡ let p = precondition_of op in
    list_all (λv. s v = Some True) p"

(* TODO effect_to_strips and effect_to_assignments could just be removed if we prove a lemma 
  showing the equivalence to effcond semantics.*)
definition effect__strips 
  :: "'variable strips_operator ⇒ ('variable, bool) Effect"
  where "effect__strips op 
    = 
      map (λv. (v, True)) (add_effects_of op)
      @ map (λv. (v, False)) (delete_effects_of op)"

definition effect_to_assignments 
  where "effect_to_assignments op ≡ effect__strips op"
(*>*)

text ‹ As discussed in \autoref{sub:serial-sas-plus-and-parallel-strips}, the effect of
a STRIPS operator can be normalized to a conjunction of atomic effects. We can therefore construct 
the successor state by simply converting the list of add effects to assignments to \<^term>‹True› resp. 
converting the list of delete effect to a list of assignments to \<^term>‹False› and then adding the 
map corresponding to the assignments to the given state \<^term>‹s› as shown below in definition 
\ref{isadef:operator-execution-strips}. 
\footnote{Function \path{effect_to_assignments} converts the operator effect to a list of 
assignments. }›

definition  execute_operator
  :: "'variable strips_state 
    ⇒ 'variable strips_operator 
    ⇒ 'variable strips_state" (infixl "⪢" 52)
  where "execute_operator s op
    ≡ s ++ map_of (effect_to_assignments op)"

end

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory STRIPS_Semantics
  imports "STRIPS_Representation"
    "List_Supplement"
    "Map_Supplement"
begin
section "STRIPS Semantics"
text ‹ Having provided a concrete implementation of STRIPS and a corresponding locale ‹strips›, we
can now continue to define the semantics of serial and parallel STRIPS plan execution (see
\autoref{sub:serial-sas-plus-and-parallel-strips} and
\autoref{sub:parallel-sas-plus-and-parallel-strips}). ›
subsection "Serial Plan Execution Semantics"

text ‹ Serial plan execution is defined by primitive recursion on the plan.
Definition \autoref{isadef:execute_serial_plan} returns the given state if the state argument does
note satisfy the precondition of the next operator in the plan.
Otherwise it executes the rest of the plan on the successor state \<^term>‹execute_operator s op› of
the given state and operator. ›

primrec  execute_serial_plan
  where "execute_serial_plan s [] = s"
  | "execute_serial_plan s (op # ops)
    = (if is_operator_applicable_in s op
      then execute_serial_plan (execute_operator s op) ops
      else s
  )"

text ‹ Analogously, a STRIPS trace either returns the singleton list containing only the given
state in case the precondition of the next operator in the plan is not satisfied. Otherwise, the
given state is prepended to trace of the rest of the plan for the successor state of executing the
next operator on the given state. ›

fun  trace_serial_plan_strips
  :: "'variable strips_state ⇒ 'variable strips_plan ⇒ 'variable strips_state list"
  where "trace_serial_plan_strips s [] = [s]"
  | "trace_serial_plan_strips s (op # ops)
      = s # (if is_operator_applicable_in s op
        then trace_serial_plan_strips (execute_operator s op) ops
        else [])"

text ‹ Finally, a serial solution is a plan which transforms a given problems initial state into
its goal state and for which all operators are elements of the problem's operator list. ›

definition  is_serial_solution_for_problem
  where "is_serial_solution_for_problem Π π
    ≡ (goal_of Π) ⊆⇩m execute_serial_plan (initial_of Π) π
      ∧ list_all (λop. ListMem op (operators_of Π)) π"

lemma is_valid_problem_strips_initial_of_dom:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
  shows "dom ((Π)⇩I) = set ((Π)⇩𝒱)"
  proof -
    {
      let ?I = "strips_problem.initial_of Π"
      let ?vs = "strips_problem.variables_of Π"
      fix v
      have "?I v ≠ None ⟷ ListMem v ?vs"
        using assms(1)
        unfolding is_valid_problem_strips_def
        by meson
      hence "v ∈ dom ?I ⟷ v ∈ set ?vs"
        using ListMem_iff
        by fast
    }
    thus ?thesis
      by auto
  qed

lemma is_valid_problem_dom_of_goal_state_is:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
  shows "dom ((Π)⇩G) ⊆ set ((Π)⇩𝒱)"
  proof -
    let ?vs = "strips_problem.variables_of Π"
    let ?G = "strips_problem.goal_of Π"
    have nb: "∀v. ?G v ≠ None ⟶ ListMem v ?vs"
      using assms(1)
      unfolding is_valid_problem_strips_def
      by meson
    {
      fix v
      assume "v ∈ dom ?G"
      then have "?G v ≠ None"
        by blast
      hence "v ∈ set ?vs"
        using nb
        unfolding ListMem_iff
        by blast
    }
    thus ?thesis
      by auto
  qed

lemma is_valid_problem_strips_operator_variable_sets:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "op ∈ set ((Π)⇩𝒪)"
  shows "set (precondition_of op) ⊆ set ((Π)⇩𝒱)"
    and "set (add_effects_of op) ⊆ set ((Π)⇩𝒱)"
    and "set (delete_effects_of op) ⊆ set ((Π)⇩𝒱)"
    and "disjnt (set (add_effects_of op)) (set (delete_effects_of op))"
  proof -
    let ?ops = "strips_problem.operators_of Π"
      and ?vs = "strips_problem.variables_of Π"
    have "list_all (is_valid_operator_strips Π) ?ops"
      using assms(1)
      unfolding is_valid_problem_strips_def
      by meson
    moreover have "∀v ∈ set (precondition_of op). v ∈ set ((Π)⇩𝒱)"
      and "∀v ∈ set (add_effects_of op). v ∈ set ((Π)⇩𝒱)"
      and "∀v ∈ set (delete_effects_of op). v ∈ set ((Π)⇩𝒱)"
      and "∀v ∈ set (add_effects_of op). v ∉ set (delete_effects_of op)"
      and "∀v ∈ set (delete_effects_of op). v ∉ set (add_effects_of op)"
      using assms(2) calculation
      unfolding is_valid_operator_strips_def list_all_iff Let_def ListMem_iff
      using variables_of_def
      by auto+
    ultimately show "set (precondition_of op) ⊆ set ((Π)⇩𝒱)"
      and "set (add_effects_of op) ⊆ set ((Π)⇩𝒱)"
      and "set (delete_effects_of op) ⊆ set ((Π)⇩𝒱)"
      and "disjnt (set (add_effects_of op)) (set (delete_effects_of op))"
      unfolding disjnt_def
      by fast+
  qed

lemma effect_to_assignments_i:
  assumes "as = effect_to_assignments op"
  shows "as =  (map (λv. (v, True)) (add_effects_of op)
      @ map (λv. (v, False)) (delete_effects_of op))"
  using assms
  unfolding effect_to_assignments_def effect__strips_def
  by auto

lemma effect_to_assignments_ii:
  ― ‹ NOTE ‹effect_to_assignments› can be simplified drastically given that only atomic effects
  and the add-effects as well as delete-effects lists only consist of variables.›
  assumes "as = effect_to_assignments op"
  obtains as⇩1 as⇩2
  where "as = as⇩1 @ as⇩2"
    and "as⇩1 = map (λv. (v, True)) (add_effects_of op)"
    and "as⇩2 = map (λv. (v, False)) (delete_effects_of op)"
  by (simp add: assms effect__strips_def effect_to_assignments_def)

― ‹ NOTE Show that for every variable ‹v› in either the add effect list or the delete effect
list, there exists an assignment in  \isaname{effect_to_assignments op} representing setting ‹v› to
true respectively setting ‹v› to false. Note that the first assumption amounts to saying that
the add effect list is not empty. This also requires us to split lemma
\isaname{effect_to_assignments_iii} into two separate lemmas since add and delete effect lists are
not required to both contain at least one variable simultaneously. ›
lemma effect_to_assignments_iii_a:
  fixes v
  assumes "v ∈ set (add_effects_of op)"
    and "as = effect_to_assignments op"
  obtains a where "a ∈ set as" "a = (v, True)"
  proof -
    let ?add_assignments = "(λv. (v, True)) ` set (add_effects_of op)"
    let ?delete_assignments = "(λv. (v, False)) ` set (delete_effects_of op)"
    obtain as⇩1 as⇩2
      where a1: "as = as⇩1 @ as⇩2"
        and a2: "as⇩1 = map (λv. (v, True)) (add_effects_of op)"
        and a3: "as⇩2 = map (λv. (v, False)) (delete_effects_of op)"
      using assms(2) effect_to_assignments_ii
      by blast
    then have b: "set as
      = ?add_assignments ∪ ?delete_assignments"
      by auto
    ― ‹ NOTE The existence of an assignment as proposed can be shown by the following sequence of
      set inclusions. ›
    {
      from b have "?add_assignments ⊆ set as"
        by blast
      moreover have "{(v, True)} ⊆ ?add_assignments"
        using assms(1) a2
        by blast
      ultimately have "∃a. a ∈ set as ∧ a = (v, True)"
        by blast
    }
    then show ?thesis
      using that
      by blast
  qed

lemma effect_to_assignments_iii_b:
  ― ‹ NOTE This proof is symmetrical to the one above. ›
  fixes v
  assumes "v ∈ set (delete_effects_of op)"
    and "as = effect_to_assignments op"
  obtains a where "a ∈ set as" "a = (v, False)"
  proof -
    let ?add_assignments = "(λv. (v, True)) ` set (add_effects_of op)"
    let ?delete_assignments = "(λv. (v, False)) ` set (delete_effects_of op)"
    obtain as⇩1 as⇩2
      where a1: "as = as⇩1 @ as⇩2"
        and a2: "as⇩1 = map (λv. (v, True)) (add_effects_of op)"
        and a3: "as⇩2 = map (λv. (v, False)) (delete_effects_of op)"
      using assms(2) effect_to_assignments_ii
      by blast
    then have b: "set as
      = ?add_assignments ∪ ?delete_assignments"
      by auto
    ― ‹ NOTE The existence of an assignment as proposed can be shown by the following sequence of
      set inclusions. ›
    {
      from b have "?delete_assignments ⊆ set as"
        by blast
      moreover have "{(v, False)} ⊆ ?delete_assignments"
        using assms(1) a2
        by blast
      ultimately have "∃a. a ∈ set as ∧ a = (v, False)"
        by blast
    }
    then show ?thesis
      using that
      by blast
  qed

lemma effect__strips_i:
  fixes op
  assumes "e = effect__strips op"
  obtains es⇩1 es⇩2
    where "e = (es⇩1 @ es⇩2)"
      and "es⇩1 = map (λv. (v, True)) (add_effects_of op)"
      and "es⇩2 = map (λv. (v, False)) (delete_effects_of op)"
  proof -
    obtain es⇩1 es⇩2 where a: "e = (es⇩1 @ es⇩2)"
      and b: "es⇩1 = map (λv. (v, True)) (add_effects_of op)"
      and c: "es⇩2 = map (λv. (v, False)) (delete_effects_of op)"
      using assms(1)
      unfolding effect__strips_def
      by blast
    then show ?thesis
      using that
      by force
  qed

lemma effect__strips_ii:
  fixes op
  assumes "e = ConjunctiveEffect (es⇩1 @ es⇩2)"
    and "es⇩1 = map (λv. (v, True)) (add_effects_of op)"
    and "es⇩2 = map (λv. (v, False)) (delete_effects_of op)"
  shows "∀v ∈ set (add_effects_of op). (∃e' ∈ set es⇩1. e' = (v, True))"
    and "∀v ∈ set (delete_effects_of op). (∃e' ∈ set es⇩2. e' = (v, False))"
  proof
  ― ‹ NOTE Show that for each variable ‹v› in the add effect list, we can obtain an atomic effect
  with true value. ›
    fix v
    {
      assume a: "v ∈ set (add_effects_of op)"
      have "set es⇩1 = (λv. (v, True)) ` set (add_effects_of op)"
        using assms(2) List.set_map
        by auto
      then obtain e'
        where "e' ∈ set es⇩1"
        and "e' =  (λv. (v, True)) v"
        using a
        by blast
      then have "∃e' ∈ set es⇩1. e' = (v, True)"
        by blast
    }
    thus "v ∈ set (add_effects_of op) ⟹ ∃e' ∈ set es⇩1. e' = (v, True)"
      by fast
  ― ‹ NOTE the proof is symmetrical to the one above: for each variable v in the delete effect list,
  we can obtain an atomic effect with v being false. ›
  next
    {
      fix v
      assume a: "v ∈ set (delete_effects_of op)"
      have "set es⇩2 = (λv. (v, False)) ` set (delete_effects_of op)"
        using assms(3) List.set_map
        by force
      then obtain e''
        where "e'' ∈ set es⇩2"
        and "e'' =  (λv. (v, False)) v"
        using a
        by blast
      then have "∃e'' ∈ set es⇩2. e'' = (v, False)"
        by blast
    }
    thus "∀v∈set (delete_effects_of op). ∃e'∈set es⇩2. e' = (v, False)"
      by fast
  qed

(* TODO refactor theory Appendix AND make visible? *)
lemma map_of_constant_assignments_dom:
  ― ‹ NOTE ancillary lemma used in the proof below. ›
  assumes "m = map_of (map (λv. (v, d)) vs)"
  shows "dom m = set vs"
  proof -
    let ?vs' = "map (λv. (v, d)) vs"
    have "dom m = fst ` set ?vs'"
      using assms(1) dom_map_of_conv_image_fst
      by metis
    moreover have "fst ` set ?vs' = set vs"
      by force
    ultimately show ?thesis
      by argo
  qed

lemma effect__strips_iii_a:
  assumes "s' = (s ⪢ op)"
  shows "⋀v. v ∈ set (add_effects_of op) ⟹ s' v = Some True"
  proof -
    fix v
    assume a: "v ∈ set (add_effects_of op)"
    let ?as = "effect_to_assignments op"
    obtain as⇩1 as⇩2 where b: "?as = as⇩1 @ as⇩2"
      and c: "as⇩1 = map (λv. (v, True)) (add_effects_of op)"
      and "as⇩2 = map (λv. (v, False)) (delete_effects_of op)"
      using effect_to_assignments_ii
      by blast
    have d: "map_of ?as = map_of as⇩2 ++ map_of as⇩1"
      using b Map.map_of_append
      by auto
    {
      ― ‹ TODO refactor? ›
      let ?vs = "add_effects_of op"
      have "?vs ≠ []"
        using a
        by force
      then have "dom (map_of as⇩1) = set (add_effects_of op)"
        using c map_of_constant_assignments_dom
        by metis
      then have "v ∈ dom (map_of as⇩1)"
        using a
        by blast
      then have "map_of ?as v = map_of as⇩1 v"
        using d
        by force
    } moreover {
      let ?f = "λ_. True"
      from c have "map_of as⇩1 = (Some ∘ ?f) |` (set (add_effects_of op))"
        using map_of_map_restrict
        by fast
      then have "map_of as⇩1 v = Some True"
        using a
        by auto
    }
    moreover have "s' = s ++ map_of as⇩2 ++ map_of as⇩1"
      using assms(1)
      unfolding execute_operator_def
      using b
      by simp
    ultimately show "s' v = Some True"
      by simp
  qed

(* TODO In contrast to the proof above we need proof preparation with auto. Why? *)
lemma effect__strips_iii_b:
  assumes "s' = (s ⪢ op)"
  shows "⋀v. v ∈ set (delete_effects_of op) ∧ v ∉ set (add_effects_of op) ⟹ s' v = Some False"
  proof (auto)
    fix v
    assume a1: "v ∉ set (add_effects_of op)" and a2: "v ∈ set (delete_effects_of op)"
    let ?as = "effect_to_assignments op"
    obtain as⇩1 as⇩2 where b: "?as = as⇩1 @ as⇩2"
      and c: "as⇩1 = map (λv. (v, True)) (add_effects_of op)"
      and d: "as⇩2 = map (λv. (v, False)) (delete_effects_of op)"
      using effect_to_assignments_ii
      by blast
    have e: "map_of ?as = map_of as⇩2 ++ map_of as⇩1"
      using b Map.map_of_append
      by auto
    {
      have "dom (map_of as⇩1) = set (add_effects_of op)"
        using c map_of_constant_assignments_dom
        by metis
      then have "v ∉ dom (map_of as⇩1)"
        using a1
        by blast
    } note f = this
    {
      let ?vs = "delete_effects_of op"
      have "?vs ≠ []"
        using a2
        by force
      then have "dom (map_of as⇩2) = set ?vs"
        using d  map_of_constant_assignments_dom
        by metis
    } note g = this
    {
      have "s' = s ++ map_of as⇩2 ++ map_of as⇩1"
        using assms(1)
        unfolding execute_operator_def
        using b
        by simp
      thm  f map_add_dom_app_simps(3)[OF f, of "s ++ map_of as⇩2"]
      moreover have "s' v = (s ++ map_of as⇩2) v"
        using calculation  map_add_dom_app_simps(3)[OF f, of "s ++ map_of as⇩2"]
        by blast
      moreover have "v ∈ dom (map_of as⇩2)"
        using a2 g
        by argo
      ultimately have "s' v = map_of as⇩2 v"
        by fastforce
    }
    moreover
    {
      let ?f = "λ_. False"
      from d have "map_of as⇩2 = (Some ∘ ?f) |` (set (delete_effects_of op))"
        using map_of_map_restrict
        by fast
      then have "map_of as⇩2 v = Some False"
        using a2
        by force
    }
    ultimately show  " s' v = Some False"
      by argo
  qed

(* TODO We need proof preparation with auto. Why? *)
lemma effect__strips_iii_c:
  assumes "s' = (s ⪢ op)"
  shows "⋀v. v ∉ set (add_effects_of op) ∧ v ∉ set (delete_effects_of op) ⟹ s' v = s v"
  proof (auto)
    fix v
    assume a1: "v ∉ set (add_effects_of op)" and a2: "v ∉ set (delete_effects_of op)"
    let ?as = "effect_to_assignments op"
    obtain as⇩1 as⇩2 where b: "?as = as⇩1 @ as⇩2"
      and c: "as⇩1 = map (λv. (v, True)) (add_effects_of op)"
      and d: "as⇩2 = map (λv. (v, False)) (delete_effects_of op)"
      using effect_to_assignments_ii
      by blast
    have e: "map_of ?as = map_of as⇩2 ++ map_of as⇩1"
      using b Map.map_of_append
      by auto
    {
      have "dom (map_of as⇩1) = set (add_effects_of op)"
        using c map_of_constant_assignments_dom
        by metis
      then have "v ∉ dom (map_of as⇩1)"
        using a1
        by blast
    } moreover  {
      have "dom (map_of as⇩2) = set (delete_effects_of op)"
        using d map_of_constant_assignments_dom
        by metis
      then have "v ∉ dom (map_of as⇩2)"
        using a2
        by blast
    }
    ultimately show "s' v = s v"
      using assms(1)
      unfolding execute_operator_def
      by (simp add: b map_add_dom_app_simps(3))
  qed

text ‹The following theorem combines three preceding sublemmas which show
that the following properties hold for the successor state ‹s' ≡ execute_operator op s›
obtained by executing an operator ‹op› in a state ‹s›:
\footnote{Lemmas \path{effect__strips_iii_a}, \path{effect__strips_iii_b}, and
\path{effect__strips_iii_c} (not shown).}

\begin{itemize}
  \item every add effect is satisfied in ‹s'› (sublemma  \isaname{effect__strips_iii_a}); and,
  \item every delete effect that is not also an add effect is not satisfied in ‹s'› (sublemma
\isaname{effect__strips_iii_b}); and finally
  \item the state remains unchanged---i.e. ‹s' v = s v›---for all variables which are neither an
add effect nor a delete effect.
\end{itemize} ›

(* TODO? Rewrite theorem ‹operator_effect__strips› to match ‹s ++ map_of (
effect_to_assignments op)› rather than ‹execute_operator Π op s› since we need this
form later on for the parallel execution theorem? *)
theorem  operator_effect__strips:
  assumes "s' = (s ⪢ op)"
  shows
    "⋀v.
      v ∈ set (add_effects_of op)
      ⟹ s' v = Some True"
    and "⋀v.
      v ∉ set (add_effects_of op) ∧ v ∈ set (delete_effects_of op)
      ⟹ s' v = Some False"
    and "⋀v.
      v ∉ set (add_effects_of op) ∧ v ∉ set (delete_effects_of op)
      ⟹ s' v = s v"
proof (auto)
  show "⋀v.
    v ∈ set (add_effects_of op)
    ⟹ s' v = Some True"
    using assms effect__strips_iii_a
    by fast
next
  show "⋀v.
    v ∉ set (add_effects_of op)
    ⟹ v ∈ set (delete_effects_of op)
    ⟹  s' v = Some False"
    using assms effect__strips_iii_b
    by fast
next
  show "⋀v.
    v ∉ set (add_effects_of op)
    ⟹ v ∉ set (delete_effects_of op)
    ⟹ s' v = s v"
    using assms effect__strips_iii_c
    by metis
qed

subsection "Parallel Plan Semantics"

definition "are_all_operators_applicable s ops
  ≡ list_all (λop. is_operator_applicable_in s op) ops"

definition "are_operator_effects_consistent op⇩1 op⇩2 ≡ let
    add⇩1 = add_effects_of op⇩1
    ; add⇩2 = add_effects_of op⇩2
    ; del⇩1 = delete_effects_of op⇩1
    ; del⇩2 = delete_effects_of op⇩2
  in ¬list_ex (λv. list_ex ((=) v) del⇩2) add⇩1 ∧ ¬list_ex (λv. list_ex ((=) v) add⇩2) del⇩1"

definition "are_all_operator_effects_consistent ops ≡
  list_all (λop. list_all (are_operator_effects_consistent op) ops) ops"

definition execute_parallel_operator
  :: "'variable strips_state
    ⇒ 'variable strips_operator list
    ⇒ 'variable strips_state"
  where "execute_parallel_operator s ops
    ≡ foldl (++) s (map (map_of ∘ effect_to_assignments) ops)"
text ‹ The parallel STRIPS execution semantics is defined in similar way as the serial STRIPS
execution semantics. However, the applicability test is lifted to parallel operators and we
additionally test for operator consistency (which was unecessary in the serial case). ›

fun  execute_parallel_plan
  :: "'variable strips_state
    ⇒ 'variable strips_parallel_plan
    ⇒ 'variable strips_state"
  where "execute_parallel_plan s [] = s"
  | "execute_parallel_plan s (ops # opss) = (if
      are_all_operators_applicable s ops
      ∧ are_all_operator_effects_consistent ops
    then execute_parallel_plan (execute_parallel_operator s ops) opss
    else s)"

definition "are_operators_interfering op⇩1 op⇩2
  ≡ list_ex (λv. list_ex ((=) v) (delete_effects_of op⇩1)) (precondition_of op⇩2)
    ∨  list_ex (λv. list_ex ((=) v) (precondition_of op⇩1)) (delete_effects_of op⇩2)"

(* TODO rewrite as inductive predicate *)
primrec are_all_operators_non_interfering
  :: "'variable strips_operator list ⇒ bool"
  where "are_all_operators_non_interfering [] = True"
  | "are_all_operators_non_interfering (op # ops)
    = (list_all (λop'. ¬are_operators_interfering op op') ops
      ∧ are_all_operators_non_interfering ops)"

text ‹ Since traces mirror the execution semantics, the same is true for the definition of
parallel STRIPS plan traces. ›

fun  trace_parallel_plan_strips
  :: "'variable strips_state ⇒ 'variable strips_parallel_plan ⇒ 'variable strips_state list"
  where "trace_parallel_plan_strips s [] = [s]"
  | "trace_parallel_plan_strips s (ops # opss) = s # (if
      are_all_operators_applicable s ops
      ∧ are_all_operator_effects_consistent ops
    then trace_parallel_plan_strips (execute_parallel_operator s ops) opss
    else [])"

text ‹ Similarly, the definition of parallel solutions requires that the parallel execution
semantics transforms the initial problem into the goal state of the problem and that every
operator of every parallel operator in the parallel plan is an operator that is defined in the
problem description. ›

definition  is_parallel_solution_for_problem
  where "is_parallel_solution_for_problem Π π
    ≡ (strips_problem.goal_of Π) ⊆⇩m execute_parallel_plan
        (strips_problem.initial_of Π) π
      ∧ list_all (λops. list_all (λop.
        ListMem op (strips_problem.operators_of Π)) ops) π"


(* TODO rename are_all_operators_applicable_in_set *)
lemma are_all_operators_applicable_set:
  "are_all_operators_applicable s ops
    ⟷ (∀op ∈ set ops. ∀v ∈ set (precondition_of op). s v = Some True)"
  unfolding are_all_operators_applicable_def
    STRIPS_Representation.is_operator_applicable_in_def list_all_iff
  by presburger

(* TODO rename are_all_operators_applicable_in_cons *)
lemma are_all_operators_applicable_cons:
  assumes "are_all_operators_applicable s (op # ops)"
  shows "is_operator_applicable_in s op"
    and "are_all_operators_applicable s ops"
  proof -
    from assms have a: "list_all (λop. is_operator_applicable_in s op) (op # ops)"
      unfolding are_all_operators_applicable_def is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def
      by blast
    then have "is_operator_applicable_in s op"
      by fastforce
    moreover {
      from a have "list_all (λop. is_operator_applicable_in s op) ops"
        by simp
      then have "are_all_operators_applicable s ops"
      using are_all_operators_applicable_def is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def
        by blast
      }
    ultimately show "is_operator_applicable_in s op"
      and "are_all_operators_applicable s ops"
       by fast+
  qed

lemma are_operator_effects_consistent_set:
  assumes "op⇩1 ∈ set ops"
    and "op⇩2 ∈ set ops"
  shows "are_operator_effects_consistent op⇩1 op⇩2
     = (set (add_effects_of op⇩1) ∩ set (delete_effects_of op⇩2) = {}
      ∧ set (delete_effects_of op⇩1) ∩ set (add_effects_of op⇩2) = {})"
  proof -
    have "(¬list_ex (λv. list_ex ((=) v) (delete_effects_of op⇩2)) (add_effects_of op⇩1))
      = (set (add_effects_of op⇩1) ∩ set (delete_effects_of op⇩2) = {})"
      using list_ex_intersection[of "delete_effects_of op⇩2" "add_effects_of op⇩1"]
      by meson
    moreover have "(¬list_ex (λv. list_ex ((=) v) (add_effects_of op⇩2)) (delete_effects_of op⇩1))
      = (set (delete_effects_of op⇩1) ∩ set (add_effects_of op⇩2) = {})"
      using list_ex_intersection[of "add_effects_of op⇩2"  "delete_effects_of op⇩1"]
      by meson
    ultimately show "are_operator_effects_consistent op⇩1 op⇩2
       = (set (add_effects_of op⇩1) ∩ set (delete_effects_of op⇩2) = {}
        ∧ set (delete_effects_of op⇩1) ∩ set (add_effects_of op⇩2) = {})"
      unfolding are_operator_effects_consistent_def
      by presburger
  qed

lemma are_all_operator_effects_consistent_set:
  "are_all_operator_effects_consistent ops
    ⟷ (∀op⇩1 ∈ set ops. ∀op⇩2 ∈ set ops.
      (set (add_effects_of op⇩1) ∩ set (delete_effects_of op⇩2) = {})
        ∧ (set (delete_effects_of op⇩1) ∩ set (add_effects_of op⇩2) = {}))"
  proof -
    {
      fix op⇩1 op⇩2
      assume "op⇩1 ∈ set ops" and "op⇩2 ∈ set ops"
      hence "are_operator_effects_consistent op⇩1 op⇩2
        = (set (add_effects_of op⇩1) ∩ set (delete_effects_of op⇩2) = {}
          ∧ set (delete_effects_of op⇩1) ∩ set (add_effects_of op⇩2) = {})"
        using are_operator_effects_consistent_set[of op⇩1 ops op⇩2]
        by fast
    }
    thus ?thesis
      unfolding are_all_operator_effects_consistent_def list_all_iff
      by force
  qed

lemma are_all_effects_consistent_tail:
  assumes "are_all_operator_effects_consistent (op # ops)"
  shows "are_all_operator_effects_consistent ops"
  proof -
    from assms
    have a: "list_all (λop'. list_all (are_operator_effects_consistent op')
      (Cons op ops)) (Cons op ops)"
      unfolding are_all_operator_effects_consistent_def
      by blast
    then have b_1: "list_all (are_operator_effects_consistent op) (op # ops)"
      and b_2: "list_all (λop'. list_all (are_operator_effects_consistent op') (op # ops)) ops"
      by force+
    then have "list_all (are_operator_effects_consistent op) ops"
      by simp
    moreover
    {
      {
        fix z
        assume "z ∈ set (Cons op ops)"
         and "list_all (are_operator_effects_consistent z) (op # ops)"
        then have "list_all (are_operator_effects_consistent z) ops"
          by auto
      }
      then have "list_all (λop'. list_all (are_operator_effects_consistent op') ops) ops"
        using list.pred_mono_strong[of
            "(λop'. list_all (are_operator_effects_consistent op') (op # ops))"
            "Cons op ops" "(λop'. list_all (are_operator_effects_consistent op')  ops)"
          ] a
        by fastforce
    }
    ultimately have "list_all (are_operator_effects_consistent op) ops
      ∧ list_all (λop'. list_all (are_operator_effects_consistent op') ops) ops"
      by blast
    then show ?thesis
      using are_all_operator_effects_consistent_def
      by fast
  qed

lemma are_all_operators_non_interfering_tail:
  assumes "are_all_operators_non_interfering (op # ops)"
  shows "are_all_operators_non_interfering ops"
  using assms
  unfolding are_all_operators_non_interfering_def
  by simp

lemma are_operators_interfering_symmetric:
  assumes "are_operators_interfering op⇩1 op⇩2"
  shows "are_operators_interfering op⇩2 op⇩1"
  using assms
  unfolding are_operators_interfering_def list_ex_iff
  by fast

― ‹ A small technical characterizing operator lists with property
\isaname{are_all_operators_non_interfering ops}. We show that pairs of distinct operators which interfere
with one another cannot both be contained in the corresponding operator set. ›
lemma are_all_operators_non_interfering_set_contains_no_distinct_interfering_operator_pairs:
  assumes "are_all_operators_non_interfering ops"
    and "are_operators_interfering op⇩1 op⇩2"
    and "op⇩1 ≠ op⇩2"
  shows "op⇩1 ∉ set ops ∨ op⇩2 ∉ set ops"
  using assms
  proof (induction ops)
    case (Cons op ops)
    thm Cons.IH[OF _ Cons.prems(2, 3)]
    have nb⇩1: "∀op' ∈ set ops. ¬are_operators_interfering op op'"
      and nb⇩2: "are_all_operators_non_interfering ops"
      using Cons.prems(1)
      unfolding are_all_operators_non_interfering.simps(2) list_all_iff
      by blast+
    then consider (A) "op = op⇩1"
      | (B) "op = op⇩2"
      | (C) "op ≠ op⇩1 ∧ op ≠ op⇩2"
      by blast
    thus ?case
      proof (cases)
        case A
        {
          assume "op⇩2 ∈ set (op # ops)"
          then have "op⇩2 ∈ set ops"
            using Cons.prems(3) A
            by force
          then have "¬are_operators_interfering op⇩1 op⇩2"
            using nb⇩1 A
            by fastforce
          hence False
            using Cons.prems(2)..
        }
        thus ?thesis
          by blast
      next
        case B
        {
          assume "op⇩1 ∈ set (op # ops)"
          then have "op⇩1 ∈ set ops"
            using Cons.prems(3) B
            by force
          then have "¬are_operators_interfering op⇩1 op⇩2"
            using nb⇩1 B are_operators_interfering_symmetric
            by blast
          hence False
            using Cons.prems(2)..
        }
        thus ?thesis
          by blast
      next
        case C
        thus ?thesis
          using Cons.IH[OF nb⇩2 Cons.prems(2, 3)]
          by force
      qed
  qed simp

(* TODO The recurring ‹list_all ↝ ∀› transformations could be refactored into a general
lemma.
   TODO refactor (also used in lemma ‹execute_serial_plan_split_i›). *)
lemma execute_parallel_plan_precondition_cons_i:
  fixes s :: "('variable, bool) state"
  assumes "¬are_operators_interfering op op'"
    and "is_operator_applicable_in s op"
    and "is_operator_applicable_in s op'"
  shows "is_operator_applicable_in (s ++ map_of (effect_to_assignments op)) op'"
  proof -
    let ?s' = "s ++ map_of (effect_to_assignments op)"
    ― ‹ TODO slightly hackish to exploit the definition of ‹execute_operator›, but we
  otherwise have to rewrite theorem ‹operator_effect__strips› (which is a todo as of now). ›
    {
      have a: "?s' = s ⪢ op"
        by (simp add: execute_operator_def)
      then have "⋀v. v ∈ set (add_effects_of op) ⟹ ?s' v = Some True"
        and "⋀v. v ∉ set (add_effects_of op) ∧ v ∈ set (delete_effects_of op) ⟹ ?s' v = Some False"
        and "⋀v. v ∉ set (add_effects_of op) ∧ v ∉ set (delete_effects_of op) ⟹ ?s' v = s v"
        using operator_effect__strips
        by metis+
    }
    note a = this
    ― ‹ TODO refactor lemma ‹not_have_interference_set›. ›
    {
      fix v
      assume α: "v ∈ set (precondition_of op')"
      {
        fix v
        have "¬list_ex ((=) v) (delete_effects_of op)
          = list_all (λv'. ¬v = v') (delete_effects_of op)"
          using not_list_ex_equals_list_all_not[
              where P="(=) v" and xs="delete_effects_of op"]
          by blast
      } moreover {
        from assms(1)
        have "¬list_ex (λv. list_ex ((=) v) (delete_effects_of op)) (precondition_of op')"
          unfolding are_operators_interfering_def
          by blast
        then have "list_all (λv. ¬list_ex ((=) v) (delete_effects_of op)) (precondition_of op')"
          using not_list_ex_equals_list_all_not[
              where P="λv. list_ex ((=) v) (delete_effects_of op)" and xs="precondition_of op'"]
          by blast
      }
      ultimately have β:
        "list_all (λv. list_all (λv'. ¬v = v') (delete_effects_of op)) (precondition_of op')"
        by presburger
      moreover {
        fix v
        have "list_all (λv'. ¬v = v') (delete_effects_of op)
          = (∀v' ∈ set (delete_effects_of op). ¬v = v')"
          using list_all_iff [where P="λv'. ¬v = v'" and x="delete_effects_of op"]
          .
      }
      ultimately have "∀v ∈ set (precondition_of op'). ∀v' ∈ set (delete_effects_of op). ¬v = v'"
        using β list_all_iff[
          where P="λv. list_all (λv'. ¬v = v') (delete_effects_of op)"
            and x="precondition_of op'"]
        by presburger
      then have "v ∉ set (delete_effects_of op)"
        using α
        by fast
    }
    note b = this
    {
      fix v
      assume a: "v ∈ set (precondition_of op')"
      have "list_all (λv. s v = Some True) (precondition_of op')"
        using assms(3)
        unfolding is_operator_applicable_in_def
          STRIPS_Representation.is_operator_applicable_in_def
        by presburger
      then have "∀v ∈ set (precondition_of op'). s v = Some True"
        using list_all_iff[where P="λv. s v = Some True" and x="precondition_of op'"]
        by blast
      then have "s v = Some True"
        using a
        by blast
    }
    note c = this
    {
      fix v
      assume d: "v ∈ set (precondition_of op')"
      then have "?s' v = Some True"
      proof (cases "v ∈ set (add_effects_of op)")
        case True
        then show ?thesis
          using a
          by blast
      next
        case e: False
        then show ?thesis
        proof (cases "v ∈ set (delete_effects_of op)")
          case True
          then show ?thesis
            using assms(1) b d
              by fast
          next
            case False
            then have "?s' v = s v"
              using a e
              by blast
            then show ?thesis
              using c d
              by presburger
          qed
      qed
    }
    then have "list_all (λv. ?s' v = Some True) (precondition_of op')"
      using list_all_iff[where P="λv. ?s' v = Some True" and x="precondition_of op'"]
      by blast
    then show ?thesis
      unfolding is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def
      by auto
  qed

― ‹ The third assumption ‹are_all_operators_non_interfering (a # ops)›" is not part of the
precondition of \isaname{execute_parallel_operator} but is required for the proof of the
subgoal hat applicable is maintained. ›
lemma execute_parallel_plan_precondition_cons:
  fixes a :: "'variable strips_operator"
  assumes "are_all_operators_applicable s (a # ops)"
    and "are_all_operator_effects_consistent (a # ops)"
    and "are_all_operators_non_interfering (a # ops)"
  shows "are_all_operators_applicable (s ++ map_of (effect_to_assignments a)) ops"
    and "are_all_operator_effects_consistent ops"
    and "are_all_operators_non_interfering ops"
  using are_all_effects_consistent_tail[OF assms(2)]
    are_all_operators_non_interfering_tail[OF assms(3)]
  proof -
    let ?s' = "s ++ map_of (effect_to_assignments a)"
    have nb⇩1: "∀op ∈ set (a # ops). is_operator_applicable_in s op"
      using assms(1) are_all_operators_applicable_set
      unfolding are_all_operators_applicable_def is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def list_all_iff
      by blast
    have nb⇩2: "∀op ∈ set ops. ¬are_operators_interfering a op"
      using assms(3)
      unfolding are_all_operators_non_interfering_def list_all_iff
      by simp
    have nb⇩3: "is_operator_applicable_in s a"
      using assms(1) are_all_operators_applicable_set
      unfolding are_all_operators_applicable_def is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def list_all_iff
      by force
    {
      fix op
      assume op_in_ops: "op ∈ set ops"
      hence "is_operator_applicable_in ?s' op"
        using execute_parallel_plan_precondition_cons_i[of a op] nb⇩1 nb⇩2 nb⇩3
        by force
    }
    then show "are_all_operators_applicable ?s' ops"
      unfolding are_all_operators_applicable_def list_all_iff
        is_operator_applicable_in_def
      by blast
  qed

lemma execute_parallel_operator_cons[simp]:
  "execute_parallel_operator s (op # ops)
    = execute_parallel_operator (s ++ map_of (effect_to_assignments op)) ops"
  unfolding execute_parallel_operator_def
  by simp

lemma execute_parallel_operator_cons_equals:
  assumes "are_all_operators_applicable s (a # ops)"
    and "are_all_operator_effects_consistent (a # ops)"
    and "are_all_operators_non_interfering (a # ops)"
  shows "execute_parallel_operator s (a # ops)
    = execute_parallel_operator (s ++ map_of (effect_to_assignments a)) ops"
  proof -
    let ?s' = "s ++ map_of (effect_to_assignments a)"
    {
      from assms(1, 2)
      have "execute_parallel_operator s (Cons a ops)
        = foldl (++) s (map (map_of ∘ effect_to_assignments) (Cons a ops))"
         unfolding execute_parallel_operator_def
         by presburger
       also have "… = foldl (++) (?s')
         (map (map_of ∘ effect_to_assignments) ops)"
         by auto
       finally have "execute_parallel_operator s (Cons a ops)
         = foldl (++) (?s')
          (map (map_of ∘ effect_to_assignments) ops)"
         using execute_parallel_operator_def
         by blast
     }
    ― ‹ NOTE the precondition of \isaname{execute_parallel} for ‹a # ops› is also true for the tail
    list and ‹state ?s'› as shown in lemma
    \isaname{execute_parallel_operator_precondition_cons}. Hence the precondition for the r.h.s.
    of the goal also holds. ›
     moreover have "execute_parallel_operator ?s' ops
        = foldl (++) (s ++ (map_of ∘ effect_to_assignments) a)
          (map (map_of ∘ effect_to_assignments) ops)"
         by (simp add: execute_parallel_operator_def)
    ultimately show ?thesis
      by force
  qed

― ‹ We show here that following the lemma above, executing one operator of a parallel
operator can be replaced by a (single) STRIPS operator execution. ›
corollary execute_parallel_operator_cons_equals_corollary:
  assumes "are_all_operators_applicable s (a # ops)"
  shows "execute_parallel_operator s (a # ops)
    = execute_parallel_operator (s ⪢ a) ops"
  proof -
    let ?s' = "s ++ map_of (effect_to_assignments a)"
    from assms
    have "execute_parallel_operator s (a # ops)
      = execute_parallel_operator (s ++ map_of (effect_to_assignments a)) ops"
      using execute_parallel_operator_cons_equals
      by simp
    moreover have "?s' = s ⪢ a"
      unfolding execute_operator_def
      by simp
    ultimately show ?thesis
      by argo
  qed

(* TODO duplicate? *)
lemma effect_to_assignments_simp[simp]: "effect_to_assignments op
  = map (λv. (v, True)) (add_effects_of op) @ map (λv. (v, False)) (delete_effects_of op)"
  by (simp add: effect_to_assignments_i)

lemma effect_to_assignments_set_is[simp]:
  "set (effect_to_assignments op) = { ((v, a), True) | v a. (v, a) ∈ set (add_effects_of op) }
    ∪ { ((v, a), False) | v a. (v, a) ∈ set (delete_effects_of op) }"
proof -
    obtain as where "effect__strips op = as"
      and "as = map (λv. (v, True)) (add_effects_of op)
        @ map (λv. (v, False)) (delete_effects_of op)"
      unfolding effect__strips_def
      by blast
    moreover have "as
      = map (λv. (v, True)) (add_effects_of op) @ map (λv. (v, False)) (delete_effects_of op)"
      using calculation(2)
      unfolding map_append map_map comp_apply
      by auto
    moreover have "effect_to_assignments op = as"
      unfolding effect_to_assignments_def calculation(1, 2)
      by auto
    ultimately show ?thesis
      unfolding set_map
      by auto
  qed

corollary effect_to_assignments_construction_from_function_graph:
  assumes "set (add_effects_of op) ∩ set (delete_effects_of op) = {}"
  shows "effect_to_assignments op = map
    (λv. (v, if ListMem v (add_effects_of op) then True else False))
    (add_effects_of op @ delete_effects_of op)"
    and "effect_to_assignments op = map
    (λv. (v, if ListMem v (delete_effects_of op) then False else True))
    (add_effects_of op @ delete_effects_of op)"
  proof -
    let ?f = "λv. (v, if ListMem v (add_effects_of op) then True else False)"
      and ?g = "λv. (v, if ListMem v (delete_effects_of op) then False else True)"
    {
      have "map ?f (add_effects_of op @ delete_effects_of op)
        = map ?f (add_effects_of op) @ map ?f (delete_effects_of op)"
        using map_append
        by fast
      ― ‹ TODO slow. ›
      hence "effect_to_assignments op = map ?f (add_effects_of op @ delete_effects_of op)"
        using ListMem_iff assms
        by fastforce
    } moreover {
      have "map ?g (add_effects_of op @ delete_effects_of op)
        = map ?g (add_effects_of op) @ map ?g (delete_effects_of op)"
        using map_append
        by fast
      ― ‹ TODO slow. ›
      hence "effect_to_assignments op = map ?g (add_effects_of op @ delete_effects_of op)"
        using ListMem_iff assms
        by fastforce
    }
    ultimately show "effect_to_assignments op = map
      (λv. (v, if ListMem v (add_effects_of op) then True else False))
      (add_effects_of op @ delete_effects_of op)"
      and "effect_to_assignments op = map
      (λv. (v, if ListMem v (delete_effects_of op) then False else True))
      (add_effects_of op @ delete_effects_of op)"
      by blast+
  qed

corollary map_of_effect_to_assignments_is_none_if:
  assumes "¬v ∈ set (add_effects_of op)"
    and "¬v ∈ set (delete_effects_of op)"
  shows "map_of (effect_to_assignments op) v = None"
  proof -
    let ?l = "effect_to_assignments op"
    {
      have "set ?l = { (v, True) | v. v ∈ set (add_effects_of op) }
        ∪ { (v, False) | v. v ∈ set (delete_effects_of op)}"
        by auto
      then have "fst ` set ?l
        = (fst ` {(v, True) | v. v ∈ set (add_effects_of op)})
          ∪ (fst ` {(v, False) | v. v ∈ set (delete_effects_of op)})"
        using image_Un[of fst "{(v, True) | v. v ∈ set (add_effects_of op)}"
           "{(v, False) | v. v ∈ set (delete_effects_of op)}"]
        by presburger
      ― ‹ TODO slow.›
      also have "… = (fst ` (λv. (v, True)) ` set (add_effects_of op))
        ∪ (fst ` (λv. (v, False)) ` set (delete_effects_of op))"
        using setcompr_eq_image[of "λv. (v, True)" "λv. v ∈ set (add_effects_of op)"]
          setcompr_eq_image[of "λv. (v, False)" "λv. v ∈ set (delete_effects_of op)"]
        by simp
      ― ‹ TODO slow.›
      also have "… = id ` set (add_effects_of op) ∪ id ` set (delete_effects_of op)"
        by force
      ― ‹ TODO slow.›
      finally have "fst ` set ?l = set (add_effects_of op) ∪ set (delete_effects_of op)"
        by auto
      hence "v ∉ fst ` set ?l"
        using assms(1, 2)
        by blast
    }
    thus ?thesis
      using map_of_eq_None_iff[of ?l v]
      by blast
  qed

lemma execute_parallel_operator_positive_effect_if_i:
  assumes "are_all_operators_applicable s ops"
    and "are_all_operator_effects_consistent ops"
    and "op ∈ set ops"
    and "v ∈ set (add_effects_of op)"
  shows "map_of (effect_to_assignments op) v = Some True"
  proof -
    let ?f = "λx. if ListMem x (add_effects_of op) then True else False"
      and ?l'= " map (λv. (v, if ListMem v (add_effects_of op) then True else False))
        (add_effects_of op @ delete_effects_of op)"
    have "set (add_effects_of op) ≠ {}"
      using assms(4)
      by fastforce
    moreover {
      have "set (add_effects_of op) ∩ set (delete_effects_of op) = {}"
        using are_all_operator_effects_consistent_set assms(2, 3)
        by fast
      moreover have "effect_to_assignments op = ?l'"
        using effect_to_assignments_construction_from_function_graph(1) calculation
        by fast
      ultimately have "map_of (effect_to_assignments op) = map_of ?l'"
        by argo
    }
    ultimately have "map_of (effect_to_assignments op) v = Some (?f v)"
      using Map_Supplement.map_of_from_function_graph_is_some_if[
          of _ _ "?f", OF _ assms(4)]
      by simp
    thus ?thesis
      using ListMem_iff assms(4)
      by metis
  qed

lemma execute_parallel_operator_positive_effect_if:
  fixes ops
  assumes "are_all_operators_applicable s ops"
    and "are_all_operator_effects_consistent ops"
    and "op ∈ set ops"
    and "v ∈ set (add_effects_of op)"
  shows "execute_parallel_operator s ops v = Some True"
  proof -
    let ?l = "map (map_of ∘ effect_to_assignments) ops"
    have set_l_is: "set ?l = (map_of ∘ effect_to_assignments) ` set ops"
      using set_map
      by fastforce
    {
      let ?m = "(map_of ∘ effect_to_assignments) op"
      have "?m ∈ set ?l"
        using assms(3) set_l_is
        by blast
      moreover have "?m v = Some True"
        using execute_parallel_operator_positive_effect_if_i[OF assms]
        by fastforce
      ultimately have "∃m ∈ set ?l. m v = Some True"
        by blast
    }
    moreover {
      fix m'
      assume "m' ∈ set ?l"
      then obtain op'
        where op'_in_set_ops: "op' ∈ set ops"
          and m'_is: "m' = (map_of ∘ effect_to_assignments) op'"
        by auto
      then have "set (add_effects_of op) ∩ set (delete_effects_of op') = {}"
        using assms(2, 3) are_all_operator_effects_consistent_set[of ops]
        by blast
      then have "v ∉ set (delete_effects_of op')"
        using assms(4)
        by blast
      then consider (v_in_set_add_effects) "v ∈ set (add_effects_of op')"
        | (otherwise) "¬v ∈ set (add_effects_of op') ∧ ¬v ∈ set (delete_effects_of op')"
        by blast
      hence "m' v = Some True ∨ m' v = None"
        proof (cases)
          case v_in_set_add_effects
          ― ‹ TODO slow. ›
          thus ?thesis
            using execute_parallel_operator_positive_effect_if_i[
                OF assms(1, 2) op'_in_set_ops, of v] m'_is
            by simp
        next
          case otherwise
          then have "¬v ∈ set (add_effects_of op')"
            and "¬v ∈ set (delete_effects_of op')"
            by blast+
          thus ?thesis
            using map_of_effect_to_assignments_is_none_if[of v op'] m'_is
            by fastforce
        qed
    }
    ― ‹ TODO slow. ›
    ultimately show ?thesis
      unfolding execute_parallel_operator_def
      using foldl_map_append_is_some_if[of s v True ?l]
      by meson
  qed

lemma execute_parallel_operator_negative_effect_if_i:
  assumes "are_all_operators_applicable s ops"
    and "are_all_operator_effects_consistent ops"
    and "op ∈ set ops"
    and "v ∈ set (delete_effects_of op)"
  shows "map_of (effect_to_assignments op) v = Some False"
  proof -
    let ?f = "λx. if ListMem x (delete_effects_of op) then False else True"
      and ?l'= " map (λv. (v, if ListMem v (delete_effects_of op) then False else True))
        (add_effects_of op @ delete_effects_of op)"
    have "set (delete_effects_of op @ add_effects_of op) ≠ {}"
      using assms(4)
      by fastforce
    moreover have "v ∈ set (delete_effects_of op @ add_effects_of op)"
      using assms(4)
      by simp
    moreover {
      have "set (add_effects_of op) ∩ set (delete_effects_of op) = {}"
        using are_all_operator_effects_consistent_set assms(2, 3)
        by fast
      moreover have "effect_to_assignments op = ?l'"
        using effect_to_assignments_construction_from_function_graph(2) calculation
        by blast
      ultimately have "map_of (effect_to_assignments op) = map_of ?l'"
        by argo
    }
    ultimately have "map_of (effect_to_assignments op) v = Some (?f v)"
      using Map_Supplement.map_of_from_function_graph_is_some_if[
          of "add_effects_of op @ delete_effects_of op" v "?f"]
      by force
    thus ?thesis
      using assms(4)
      unfolding ListMem_iff
      by presburger
  qed

lemma execute_parallel_operator_negative_effect_if:
  assumes "are_all_operators_applicable s ops"
    and "are_all_operator_effects_consistent ops"
    and "op ∈ set ops"
    and "v ∈ set (delete_effects_of op)"
  shows "execute_parallel_operator s ops v = Some False"
  proof -
    let ?l = "map (map_of ∘ effect_to_assignments) ops"
    have set_l_is: "set ?l = (map_of ∘ effect_to_assignments) ` set ops"
      using set_map
      by fastforce
    {
      let ?m = "(map_of ∘ effect_to_assignments) op"
      have "?m ∈ set ?l"
        using assms(3) set_l_is
        by blast
      moreover have "?m v = Some False"
        using execute_parallel_operator_negative_effect_if_i[OF assms]
        by fastforce
      ultimately have "∃m ∈ set ?l. m v = Some False"
        by blast
    }
    moreover {
      fix m'
      assume "m' ∈ set ?l"
      then obtain op'
        where op'_in_set_ops: "op' ∈ set ops"
          and m'_is: "m' = (map_of ∘ effect_to_assignments) op'"
        by auto
      then have "set (delete_effects_of op) ∩ set (add_effects_of op') = {}"
        using assms(2, 3) are_all_operator_effects_consistent_set[of ops]
        by blast
      then have "v ∉ set (add_effects_of op')"
        using assms(4)
        by blast
      then consider (v_in_set_delete_effects) "v ∈ set (delete_effects_of op')"
        | (otherwise) "¬v ∈ set (add_effects_of op') ∧ ¬v ∈ set (delete_effects_of op')"
        by blast
      hence "m' v = Some False ∨ m' v = None"
        proof (cases)
          case v_in_set_delete_effects
          ― ‹ TODO slow. ›
          thus ?thesis
            using execute_parallel_operator_negative_effect_if_i[
                OF assms(1, 2) op'_in_set_ops, of v] m'_is
            by simp
        next
          case otherwise
          then have "¬v ∈ set (add_effects_of op')"
            and "¬v ∈ set (delete_effects_of op')"
            by blast+
          thus ?thesis
            using map_of_effect_to_assignments_is_none_if[of v op'] m'_is
            by fastforce
        qed
    }
    ― ‹ TODO slow. ›
    ultimately show ?thesis
      unfolding execute_parallel_operator_def
      using foldl_map_append_is_some_if[of s v False ?l]
      by meson
  qed

lemma execute_parallel_operator_no_effect_if:
  assumes "∀op ∈ set ops. ¬v ∈ set (add_effects_of op) ∧ ¬v ∈ set (delete_effects_of op)"
  shows "execute_parallel_operator s ops v = s v"
  using assms
  unfolding execute_parallel_operator_def
  proof (induction ops arbitrary: s)
    case (Cons a ops)
    let ?f = "map_of ∘ effect_to_assignments"
    {
      have "v ∉ set (add_effects_of a) ∧ v ∉ set (delete_effects_of a)"
        using Cons.prems(1)
        by force
      then have "?f a v = None"
        using map_of_effect_to_assignments_is_none_if[of v a]
        by fastforce
      then have "v ∉ dom (?f a)"
        by blast
      hence "(s ++ ?f a) v = s v"
        using map_add_dom_app_simps(3)[of v "?f a" s]
        by blast
    }
    moreover {
      have "∀op∈set ops. v ∉ set (add_effects_of op) ∧ v ∉ set (delete_effects_of op)"
        using Cons.prems(1)
        by simp
      hence "foldl (++) (s ++ ?f a) (map ?f ops) v = (s ++ ?f a) v"
        using Cons.IH[of "s ++ ?f a"]
        by blast
    }
    moreover {
      have "map ?f (a # ops) = ?f a # map ?f ops"
        by force
      then have "foldl (++) s (map ?f (a # ops))
        = foldl (++) (s ++ ?f a) (map ?f ops)"
        using foldl_Cons
        by force
    }
    ultimately show ?case
      by argo
  qed fastforce

corollary execute_parallel_operators_strips_none_if:
  assumes "∀op ∈ set ops. ¬v ∈ set (add_effects_of op) ∧ ¬v ∈ set (delete_effects_of op)"
    and "s v = None"
  shows "execute_parallel_operator s ops v = None"
  using execute_parallel_operator_no_effect_if[OF assms(1)] assms(2)
  by simp

corollary execute_parallel_operators_strips_none_if_contraposition:
  assumes "¬execute_parallel_operator s ops v = None"
  shows "(∃op ∈ set ops. v ∈ set (add_effects_of op) ∨ v ∈ set (delete_effects_of op))
    ∨ s v ≠ None"
  proof -
    let ?P = "(∀op ∈ set ops. ¬v ∈ set (add_effects_of op) ∧ ¬v ∈ set (delete_effects_of op))
      ∧ s v = None"
      and ?Q = "execute_parallel_operator s ops v = None"
    have "?P ⟹ ?Q"
      using execute_parallel_operators_strips_none_if[of ops v s]
      by blast
    then have "¬?P"
      using contrapos_nn[of ?Q ?P]
      using assms
      by argo
    thus ?thesis
      by meson
  qed

text ‹ We will now move on to showing the equivalent to theorem \isaname{operator_effect__strips}
in \isaname{execute_parallel_operator_effect}.
Under the condition that for a list of operators \<^term>‹ops› all
operators in the corresponding set are applicable in a given state \<^term>‹s› and all operator effects
are consistent, if an operator \<^term>‹op› exists with \<^term>‹op ∈ set ops› and with \<^term>‹v› being
an add effect of \<^term>‹op›, then the successor state

  @{text[display, indent=4] "s' ≡ execute_parallel_operator s ops"}

will evaluate \<^term>‹v› to true, that is

  @{text[display, indent=4] "execute_parallel_operator s ops v = Some True"}

Symmetrically, if \<^term>‹v› is a delete effect, we have

  @{text[display, indent=4] "execute_parallel_operator s ops v = Some False"}

under the same condition as for the positive effect.
Lastly, if \<^term>‹v› is neither an add effect nor a delete effect for any operator in the
operator set corresponding to $ops$, then the state after parallel operator execution remains
unchanged, i.e.

  @{text[display, indent=4] "execute_parallel_operator s ops v = s v"}
›

theorem  execute_parallel_operator_effect:
  assumes "are_all_operators_applicable s ops"
  and "are_all_operator_effects_consistent ops"
shows "op ∈ set ops ∧ v ∈ set (add_effects_of op)
  ⟶ execute_parallel_operator s ops v = Some True"
  and "op ∈ set ops ∧ v ∈ set (delete_effects_of op)
    ⟶ execute_parallel_operator s ops v = Some False"
  and "(∀op ∈ set ops.
    v ∉ set (add_effects_of op) ∧ v ∉ set (delete_effects_of op))
    ⟶ execute_parallel_operator s ops v = s v"
  using execute_parallel_operator_positive_effect_if[OF assms]
    execute_parallel_operator_negative_effect_if[OF assms]
    execute_parallel_operator_no_effect_if[of ops v s]
  by blast+


lemma is_parallel_solution_for_problem_operator_set:
  fixes Π:: "'a strips_problem"
  assumes "is_parallel_solution_for_problem Π π"
    and "ops ∈ set π"
    and "op ∈ set ops"
  shows "op ∈ set ((Π)⇩𝒪)"
  proof -
    have "∀ops ∈ set π. ∀op ∈ set ops. op ∈ set (strips_problem.operators_of Π)"
      using assms(1)
      unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff..
    thus ?thesis
      using assms(2, 3)
      by fastforce
  qed

lemma trace_parallel_plan_strips_not_nil: "trace_parallel_plan_strips I π ≠ []"
  proof (cases π)
    case (Cons a list)
    then show ?thesis
      by (cases "are_all_operators_applicable I (hd π) ∧ are_all_operator_effects_consistent (hd π)"
        , simp+)
  qed simp

corollary length_trace_parallel_plan_gt_0[simp]: "0 < length (trace_parallel_plan_strips I π)"
  using trace_parallel_plan_strips_not_nil..

corollary length_trace_minus_one_lt_length_trace[simp]:
  "length (trace_parallel_plan_strips I π) - 1 < length (trace_parallel_plan_strips I π)"
  using diff_less[OF _ length_trace_parallel_plan_gt_0]
  by auto

lemma trace_parallel_plan_strips_head_is_initial_state:
  "trace_parallel_plan_strips I π ! 0 = I"
  proof  (cases π)
    case (Cons a list)
    then show ?thesis
      by (cases "are_all_operators_applicable I a ∧ are_all_operator_effects_consistent a", simp+)
  qed simp

lemma trace_parallel_plan_strips_length_gt_one_if:
  assumes "k < length (trace_parallel_plan_strips I π) - 1"
  shows "1 < length (trace_parallel_plan_strips I π)"
  using assms
  by linarith

― ‹ This lemma simply shows that the last element of a ‹trace_parallel_plan_strips execution›
‹step s # trace_parallel_plan_strips s' π› always is the last element of
‹trace_parallel_plan_strips s' π› since ‹trace_parallel_plan_strips› always returns at least a
singleton list (even if ‹π = []›). ›
lemma trace_parallel_plan_strips_last_cons_then:
  "last (s # trace_parallel_plan_strips s' π) = last (trace_parallel_plan_strips s' π)"
  by (cases π, simp, force)

text ‹ Parallel plan traces have some important properties that we want to confirm before
proceeding. Let \<^term>‹τ ≡ trace_parallel_plan_strips I π› be a trace for a parallel plan \<^term>‹π›
with initial state \<^term>‹I›.

First, all parallel operators \<^term>‹ops = π ! k› for any index \<^term>‹k› with \<^term>‹k < length τ - 1›
(meaning that \<^term>‹k› is not the index of the last element).
must be applicable and their effects must be consistent. Otherwise, the trace would have terminated
and \<^term>‹ops› would have been the last element. This would violate the assumption that \<^term>‹k < length τ - 1›
is not the last index since the index of the last element is \<^term>‹length τ - 1›.
\footnote{More precisely, the index of the last element is \<^term>‹length τ - 1› if \<^term>‹τ› is not
empty which is however always true since the trace contains at least the initial state.} ›

(* TODO? hide? *)
lemma  trace_parallel_plan_strips_operator_preconditions:
  assumes "k < length (trace_parallel_plan_strips I π) - 1"
  shows "are_all_operators_applicable (trace_parallel_plan_strips I π ! k) (π ! k)
      ∧ are_all_operator_effects_consistent (π ! k)"
  using assms
  proof  (induction "π" arbitrary: I k)
    ― ‹ NOTE Base case yields contradiction with assumption and can be left to automation. ›
    case (Cons a π)
    then show ?case
      proof (cases "are_all_operators_applicable I a ∧ are_all_operator_effects_consistent a")
        case True
        have trace_parallel_plan_strips_cons: "trace_parallel_plan_strips I (a # π)
          = I # trace_parallel_plan_strips (execute_parallel_operator I a) π"
          using True
          by simp
        then show ?thesis
        proof (cases "k")
          case 0
          have "trace_parallel_plan_strips I (a # π) ! 0 = I"
            using trace_parallel_plan_strips_cons
            by simp
          moreover have "(a # π) ! 0 = a"
            by simp
          ultimately show ?thesis
            using True 0
            by presburger
        next
          case (Suc k')
          let ?I' = "execute_parallel_operator I a"
          have "trace_parallel_plan_strips I (a # π) ! Suc k' = trace_parallel_plan_strips ?I' π ! k'"
            using trace_parallel_plan_strips_cons
            by simp
          moreover have "(a # π) ! Suc k' = π ! k'"
            by simp
          moreover {
            have "length (trace_parallel_plan_strips I (a # π))
              = 1 + length (trace_parallel_plan_strips ?I' π)"
              unfolding trace_parallel_plan_strips_cons
              by simp
            then have "k' < length (trace_parallel_plan_strips ?I' π) - 1"
              using Suc Cons.prems
              by fastforce
            hence "are_all_operators_applicable (trace_parallel_plan_strips ?I' π ! k') (π ! k')
            ∧ are_all_operator_effects_consistent (π ! k')"
              using Cons.IH[of k']
              by blast
          }
          ultimately show ?thesis
            using Suc
            by argo
        qed
      next
        case False
        then have "trace_parallel_plan_strips I (a # π) = [I]"
          by force
        then have "length (trace_parallel_plan_strips I (a # π)) - 1 = 0"
          by simp
        ― ‹ NOTE Thesis follows from contradiction with assumption. ›
        then show ?thesis
          using Cons.prems
          by force
      qed
  qed auto

text ‹ Another interesting property that we verify below is that elements of the trace
store the result of plan prefix execution. This means that for an index \<^term>‹k› with\newline
\<^term>‹k < length (trace_parallel_plan_strips I π)›, the \<^term>‹k›-th element of the trace is state
reached by executing the plan prefix \<^term>‹take k π› consisting of the first \<^term>‹k› parallel
operators of \<^term>‹π›. ›

lemma  trace_parallel_plan_plan_prefix:
  assumes "k < length (trace_parallel_plan_strips I π)"
  shows "trace_parallel_plan_strips I π ! k = execute_parallel_plan I (take k π)"
  using assms
  proof  (induction π arbitrary: I k)
    case (Cons a π)
    then show ?case
      proof (cases "are_all_operators_applicable I a ∧ are_all_operator_effects_consistent a")
        case True
        let ?σ = "trace_parallel_plan_strips I (a # π)"
          and ?I' = "execute_parallel_operator I a"
        have σ_equals: "?σ = I # trace_parallel_plan_strips ?I' π"
          using True
          by auto
        then show ?thesis
          proof (cases "k = 0")
            case False
            obtain k' where k_is_suc_of_k': "k = Suc k'"
              using not0_implies_Suc[OF False]
              by blast
            then have "execute_parallel_plan I (take k (a # π))
              = execute_parallel_plan ?I' (take k' π)"
              using True
              by simp
            moreover have "trace_parallel_plan_strips I (a # π) ! k
              = trace_parallel_plan_strips ?I' π ! k'"
              using σ_equals k_is_suc_of_k'
              by simp
            moreover {
              have "k' < length (trace_parallel_plan_strips (execute_parallel_operator I a) π)"
                using Cons.prems σ_equals k_is_suc_of_k'
                by force
              hence "trace_parallel_plan_strips ?I' π ! k'
                = execute_parallel_plan ?I' (take k' π)"
                using Cons.IH[of k' ?I']
                by blast
            }
            ultimately show ?thesis
              by presburger
          qed simp
      next
        case operator_precondition_violated: False
        then show ?thesis
        proof (cases "k = 0")
          case False
          then have "trace_parallel_plan_strips I (a # π) = [I]"
            using operator_precondition_violated
            by force
          moreover have "execute_parallel_plan I (take k (a # π)) = I"
            using Cons.prems operator_precondition_violated
            by force
          ultimately show ?thesis
            using Cons.prems nth_Cons_0
            by auto
        qed simp
      qed
  qed simp


lemma length_trace_parallel_plan_strips_lte_length_plan_plus_one:
  shows "length (trace_parallel_plan_strips I π) ≤ length π + 1"
  proof (induction π arbitrary: I)
    case (Cons a π)
    then show ?case
      proof (cases "are_all_operators_applicable I a ∧ are_all_operator_effects_consistent a")
        case True
        let ?I' = "execute_parallel_operator I a"
        {
          have "trace_parallel_plan_strips I (a # π) = I # trace_parallel_plan_strips ?I' π"
            using True
            by auto
          then have "length (trace_parallel_plan_strips I (a # π))
            = length (trace_parallel_plan_strips ?I' π) + 1"
            by simp
          moreover have "length (trace_parallel_plan_strips ?I' π) ≤ length π + 1"
            using Cons.IH[of ?I']
            by blast
          ultimately have "length (trace_parallel_plan_strips I (a # π)) ≤ length (a # π) + 1"
            by simp
        }
        thus ?thesis
          by blast
      qed auto
  qed simp

― ‹ Show that ‹π› is at least a singleton list. ›
lemma plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements:
  assumes "k < length (trace_parallel_plan_strips I π) - 1"
  obtains ops π' where "π = ops # π'"
  proof -
    let ?τ = "trace_parallel_plan_strips I π"
    have "length ?τ ≤ length π + 1"
      using length_trace_parallel_plan_strips_lte_length_plan_plus_one
      by fast
    then have "0 < length π"
      using trace_parallel_plan_strips_length_gt_one_if assms
      by force
    then obtain k' where "length π = Suc k'"
      using gr0_implies_Suc
      by meson
    thus ?thesis using that
      using length_Suc_conv[of π k']
      by blast
  qed

― ‹ Show that if a parallel plan trace does not have maximum length, in the last state
reached through operator execution the parallel operator execution condition was violated. ›
corollary length_trace_parallel_plan_strips_lt_length_plan_plus_one_then:
  assumes "length (trace_parallel_plan_strips I π) < length π + 1"
  shows "¬are_all_operators_applicable
      (execute_parallel_plan I (take (length (trace_parallel_plan_strips I π) - 1) π))
      (π ! (length (trace_parallel_plan_strips I π) - 1))
    ∨ ¬are_all_operator_effects_consistent (π ! (length (trace_parallel_plan_strips I π) - 1))"
  using assms
  proof (induction π arbitrary: I)
    case (Cons ops π)
    let ?τ = "trace_parallel_plan_strips I (ops # π)"
      and ?I' = "execute_parallel_operator I ops"
    show ?case
      proof (cases "are_all_operators_applicable I ops ∧ are_all_operator_effects_consistent ops")
        case True
        then have τ_is: "?τ = I # trace_parallel_plan_strips ?I' π"
          by fastforce
        show ?thesis
          proof (cases "length (trace_parallel_plan_strips ?I' π) < length π + 1")
            case True
            then have "¬ are_all_operators_applicable
              (execute_parallel_plan ?I'
                (take (length (trace_parallel_plan_strips ?I' π) - 1) π))
              (π ! (length (trace_parallel_plan_strips ?I' π) - 1))
            ∨ ¬ are_all_operator_effects_consistent
              (π ! (length (trace_parallel_plan_strips ?I' π) - 1))"
              using Cons.IH[of ?I']
              by blast
            moreover have "trace_parallel_plan_strips ?I' π ≠ []"
              using trace_parallel_plan_strips_not_nil
              by blast
            ultimately show ?thesis
              unfolding take_Cons'
              by simp
          next
            case False
            then have "length (trace_parallel_plan_strips ?I' π) ≥ length π + 1"
              by fastforce
            thm Cons.prems
            moreover have "length (trace_parallel_plan_strips I (ops # π))
              = 1 + length (trace_parallel_plan_strips ?I' π)"
              using True
              by force
            moreover have "length (trace_parallel_plan_strips ?I' π)
              < length (ops # π)"
              using Cons.prems calculation(2)
              by force
            ultimately have False
              by fastforce
            thus ?thesis..
          qed
      next
        case False
        then have τ_is_singleton: "?τ = [I]"
          using False
          by auto
        then have "ops = (ops # π) ! (length ?τ - 1)"
          by fastforce
        moreover have "execute_parallel_plan I (take (length ?τ - 1) π) = I"
          using τ_is_singleton
          by auto
        ― ‹ TODO slow. ›
        ultimately show ?thesis
          using False
          by auto
      qed
  qed simp

lemma trace_parallel_plan_step_effect_is:
  assumes "k < length (trace_parallel_plan_strips I π) - 1"
  shows "trace_parallel_plan_strips I π ! Suc k
    = execute_parallel_operator (trace_parallel_plan_strips I π ! k) (π ! k)"
  proof -
    ― ‹ NOTE Rewrite the proposition using lemma ‹trace_parallel_plan_strips_subplan›. ›
    {
      let ?τ = "trace_parallel_plan_strips I π"
      have "Suc k < length ?τ"
        using assms
        by linarith
      hence "trace_parallel_plan_strips I π ! Suc k
        = execute_parallel_plan I (take (Suc k) π)"
        using trace_parallel_plan_plan_prefix[of "Suc k" I π]
        by blast
    }
    moreover have "execute_parallel_plan I (take (Suc k) π)
      = execute_parallel_operator (trace_parallel_plan_strips I π ! k) (π ! k)"
      using assms
      proof (induction k arbitrary: I π)
        case 0
        then have "execute_parallel_operator (trace_parallel_plan_strips I π ! 0) (π ! 0)
            = execute_parallel_operator I (π ! 0)"
          using trace_parallel_plan_strips_head_is_initial_state[of I π]
          by argo
        moreover {
          obtain ops π' where "π = ops # π'"
            using plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements[OF "0.prems"]
            by blast
          then have "take (Suc 0) π = [π ! 0]"
            by simp
          hence "execute_parallel_plan I (take (Suc 0) π)
            = execute_parallel_plan I [π ! 0]"
            by argo
        }
        moreover {
          have "0 < length (trace_parallel_plan_strips I π) - 1"
            using trace_parallel_plan_strips_length_gt_one_if "0.prems"
            by fastforce
          hence "are_all_operators_applicable I (π ! 0)
            ∧ are_all_operator_effects_consistent (π ! 0)"
            using trace_parallel_plan_strips_operator_preconditions[of 0 I π]
              trace_parallel_plan_strips_head_is_initial_state[of I π]
            by argo
        }
        ultimately show ?case
          by auto
      next
        case (Suc k)
        obtain ops π' where π_split: "π = ops # π'"
          using plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements[OF Suc.prems]
          by blast
        let ?I' = "execute_parallel_operator I ops"
        {
          have "length (trace_parallel_plan_strips I π) =
            1 + length (trace_parallel_plan_strips ?I' π')"
            using Suc.prems π_split
            by fastforce
          then have "k < length (trace_parallel_plan_strips ?I' π')"
            using Suc.prems
            by fastforce
          moreover have "trace_parallel_plan_strips I π ! Suc k
            = trace_parallel_plan_strips ?I' π' ! k"
            using Suc.prems π_split
            by force
          ultimately have "trace_parallel_plan_strips I π ! Suc k
            = execute_parallel_plan ?I' (take k π')"
            using trace_parallel_plan_plan_prefix[of k ?I' π']
            by argo
        }
        moreover have "execute_parallel_plan I (take (Suc (Suc k)) π)
          = execute_parallel_plan ?I' (take (Suc k) π')"
          using Suc.prems π_split
          by fastforce
        moreover {
          have "0 < length (trace_parallel_plan_strips I π) - 1"
            using Suc.prems
            by linarith
          hence "are_all_operators_applicable I (π ! 0)
            ∧ are_all_operator_effects_consistent (π ! 0)"
            using trace_parallel_plan_strips_operator_preconditions[of 0 I π]
              trace_parallel_plan_strips_head_is_initial_state[of I π]
            by argo
        }
        ultimately show ?case
          using Suc.IH Suc.prems π_split
          by auto
      qed
    ultimately show ?thesis
      using assms
      by argo
  qed

― ‹ Show that every state in a plan execution trace of a valid problem description is defined
for all problem variables. This is true because the initial state is defined for all problem
variables—by definition of @{text "is_valid_problem_strips Π"}—and no operator can remove a
previously defined variable (only positive and negative effects are possible). ›
(* TODO refactor ‹STRIPS_Semantics› + abstract/concretize first two assumptions (e.g. second one
only needs all operators are problem operators)? *)
lemma trace_parallel_plan_strips_none_if:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "is_parallel_solution_for_problem Π π"
    and "k < length (trace_parallel_plan_strips ((Π)⇩I) π)"
  shows "(trace_parallel_plan_strips ((Π)⇩I) π ! k) v = None ⟷ v ∉ set ((Π)⇩𝒱)"
  proof -
    let ?vs = "strips_problem.variables_of Π"
      and ?ops = "strips_problem.operators_of Π"
      and ?τ = "trace_parallel_plan_strips ((Π)⇩I) π"
      and ?I = "strips_problem.initial_of Π"
    show ?thesis
      using assms
      proof (induction k)
        case 0
        have "?τ ! 0 = ?I"
          using trace_parallel_plan_strips_head_is_initial_state
          by auto
        then show ?case
          using is_valid_problem_strips_initial_of_dom[OF assms(1)]
          by auto
      next
        case (Suc k)
        have k_lt_length_τ_minus_one: "k < length ?τ - 1"
          using Suc.prems(3)
          by linarith
        then have IH: "(trace_parallel_plan_strips ?I π ! k) v = None ⟷ v ∉set ((Π)⇩𝒱)"
          using Suc.IH[OF Suc.prems(1, 2)]
          by force
        have τ_Suc_k_is: "(?τ ! Suc k) = execute_parallel_operator (?τ ! k) (π ! k)"
          using trace_parallel_plan_step_effect_is[OF k_lt_length_τ_minus_one].
        have all_operators_applicable: "are_all_operators_applicable (?τ ! k) (π ! k)"
          and all_effects_consistent: "are_all_operator_effects_consistent (π ! k)"
          using trace_parallel_plan_strips_operator_preconditions[OF k_lt_length_τ_minus_one]
          by simp+
        show ?case
          proof (rule iffI)
            assume τ_Suc_k_of_v_is_None: "(?τ ! Suc k) v = None"
            show "v ∉ set ((Π)⇩𝒱)"
              proof (rule ccontr)
                assume "¬v ∉ set ((Π)⇩𝒱)"
                then have v_in_set_vs: "v ∈ set((Π)⇩𝒱)"
                  by blast
                show False
                  proof (cases "∃op ∈ set (π ! k).
                    v ∈ set (add_effects_of op) ∨ v ∈ set (delete_effects_of op)")
                    case True
                    then obtain op
                      where op_in_π⇩k: "op ∈ set (π ! k)"
                        and "v ∈ set (add_effects_of op) ∨ v ∈ set (delete_effects_of op)"..
                    then consider (A) "v ∈ set (add_effects_of op)"
                      | (B) "v ∈ set (delete_effects_of op)"
                      by blast
                    thus False
                      using execute_parallel_operator_positive_effect_if[OF
                              all_operators_applicable all_effects_consistent op_in_π⇩k]
                            execute_parallel_operator_negative_effect_if[OF
                              all_operators_applicable all_effects_consistent op_in_π⇩k]
                            τ_Suc_k_of_v_is_None τ_Suc_k_is
                      by (cases, fastforce+)
                  next
                    case False
                    then have "∀op ∈ set (π ! k).
                      v ∉ set (add_effects_of op) ∧ v ∉ set (delete_effects_of op)"
                      by blast
                    then have "(?τ ! Suc k) v = (?τ ! k) v"
                      using execute_parallel_operator_no_effect_if τ_Suc_k_is
                      by fastforce
                    then have "v ∉ set ((Π)⇩𝒱)"
                      using IH  τ_Suc_k_of_v_is_None
                      by simp
                    thus False
                      using v_in_set_vs
                      by blast
                  qed
              qed
          next
            assume v_notin_vs: "v ∉ set ((Π)⇩𝒱)"
            {
              fix op
              assume op_in_π⇩k: "op ∈ set (π ! k)"
              {
                have "1 < length ?τ"
                  using trace_parallel_plan_strips_length_gt_one_if[OF k_lt_length_τ_minus_one].
                then have "0 < length ?τ - 1"
                  using k_lt_length_τ_minus_one
                  by linarith
                moreover have "length ?τ - 1 ≤ length π"
                  using length_trace_parallel_plan_strips_lte_length_plan_plus_one le_diff_conv
                  by blast
                then have "k < length π"
                  using k_lt_length_τ_minus_one
                  by force
                hence "π ! k ∈ set π"
                  by simp
              }
              then have op_in_ops: "op ∈ set ?ops"
                using is_parallel_solution_for_problem_operator_set[OF assms(2) _ op_in_π⇩k]
                by force
              hence "v ∉ set (add_effects_of op)" and "v ∉ set (delete_effects_of op)"
                subgoal
                  using is_valid_problem_strips_operator_variable_sets(2) assms(1) op_in_ops
                    v_notin_vs
                  by auto
                subgoal
                  using is_valid_problem_strips_operator_variable_sets(3) assms(1) op_in_ops
                    v_notin_vs
                  by auto
                done
            }
            then have "(?τ ! Suc k) v = (?τ ! k) v"
              using execute_parallel_operator_no_effect_if τ_Suc_k_is
              by metis
            thus "(?τ ! Suc k) v = None"
              using IH v_notin_vs
              by fastforce
          qed
      qed
  qed

text ‹ Finally, given initial and goal states \<^term>‹I› and \<^term>‹G›, we can show that it's
equivalent to say that \<^term>‹π› is a solution for \<^term>‹I› and \<^term>‹G›---i.e.
\<^term>‹G ⊆⇩m execute_parallel_plan I π›---and
that the goal state is subsumed by the last element of the trace of \<^term>‹π› with initial state
\<^term>‹I›. ›

lemma  execute_parallel_plan_reaches_goal_iff_goal_is_last_element_of_trace:
  "G ⊆⇩m execute_parallel_plan I π
    ⟷ G ⊆⇩m last (trace_parallel_plan_strips I π)"
  proof  -
    let ?LHS = "G ⊆⇩m execute_parallel_plan I π"
      and ?RHS = "G ⊆⇩m last (trace_parallel_plan_strips I π)"
    show ?thesis
      proof (rule iffI)
        assume ?LHS
        thus ?RHS
          proof (induction π arbitrary: I)
            ― ‹ NOTE Nil case follows from simplification. ›
            case (Cons a π)
            thus ?case
              using Cons.prems
              proof (cases "are_all_operators_applicable I a ∧ are_all_operator_effects_consistent a")
                case True
                let ?I' = "execute_parallel_operator I a"
                {
                  have "execute_parallel_plan I (a # π) = execute_parallel_plan ?I' π"
                    using True
                    by auto
                  then have "G ⊆⇩m execute_parallel_plan ?I' π"
                    using Cons.prems
                    by presburger
                  hence "G ⊆⇩m last (trace_parallel_plan_strips ?I' π)"
                    using Cons.IH[of ?I']
                    by blast
                }
                moreover {
                  have "trace_parallel_plan_strips I (a # π)
                    = I # trace_parallel_plan_strips ?I' π"
                    using True
                    by simp
                  then have "last (trace_parallel_plan_strips I (a # π))
                    = last (I # trace_parallel_plan_strips ?I' π)"
                    by argo
                  hence "last (trace_parallel_plan_strips I (a # π))
                    = last (trace_parallel_plan_strips ?I' π)"
                    using trace_parallel_plan_strips_last_cons_then[of I ?I' π]
                    by argo
                }
                ultimately show ?thesis
                  by argo
              qed force
            qed simp
      next
        assume ?RHS
        thus ?LHS
          proof (induction π arbitrary: I)
            ― ‹ NOTE Nil case follows from simplification. ›
            case (Cons a π)
            thus ?case
              proof (cases "are_all_operators_applicable I a ∧ are_all_operator_effects_consistent a")
                case True
                let ?I' = "execute_parallel_operator I a"
                {
                  have "trace_parallel_plan_strips I (a # π) = I # (trace_parallel_plan_strips ?I' π)"
                    using True
                    by simp
                  then have "last (trace_parallel_plan_strips I (a # π))
                    = last (trace_parallel_plan_strips ?I' π)"
                    using trace_parallel_plan_strips_last_cons_then[of I ?I' π]
                    by argo
                  hence "G ⊆⇩m last (trace_parallel_plan_strips ?I' π)"
                    using Cons.prems
                    by argo
                }
                thus ?thesis
                  using True Cons
                  by simp
              next
                case False
                then have "last (trace_parallel_plan_strips I (a # π)) = I"
                  and "execute_parallel_plan I (a # π) = I"
                  by (fastforce, force)
                thus ?thesis
                  using Cons.prems
                  by argo
              qed
          qed fastforce
      qed
  qed

subsection "Serializable Parallel Plans"

text ‹ With the groundwork on parallel and serial execution of STRIPS in place we can now address
the question under which conditions a parallel solution to a problem corresponds to a serial
solution and vice versa.
As we will see (in theorem \ref{isathm:embedding-serial-strips-plan}), while a serial plan can
be trivially rewritten as a parallel plan consisting of singleton operator list for each operator
in the plan, the condition for parallel plan solutions also involves non interference. ›


― ‹ Given that non interference implies that operator execution order can be switched
arbitrarily, it stands to reason that parallel operator execution can be serialized if non
interference is mandated in addition to the regular parallel execution condition (applicability and
effect consistency). This is in fact true as we show in the lemma below
\footnote{In the source literatur it is required that $\mathrm{app}_S(s)$ is defined which requires that
$\mathrm{app}_o(s)$ is defined for every $o \in S$. This again means that the preconditions
hold in $s$ and the set of effects is consistent which translates to the execution condition
in ‹execute_parallel_operator›.
\cite[Lemma 2.11., p.1037]{DBLP:journals/ai/RintanenHN06}

Also, the proposition \cite[Lemma 2.11., p.1037]{DBLP:journals/ai/RintanenHN06} is in fact
proposed to be true for any total ordering of the operator set but we only proof it for the
implicit total ordering induced by the specific order in the operator list of the problem
statement.} ›
(* TODO rename execute_parallel_operator_equals_execute_serial_if *)
lemma execute_parallel_operator_equals_execute_sequential_strips_if:
  fixes s :: "('variable, bool) state"
  assumes "are_all_operators_applicable s ops"
    and "are_all_operator_effects_consistent ops"
    and "are_all_operators_non_interfering ops"
  shows "execute_parallel_operator s ops = execute_serial_plan s ops"
  using assms
  proof (induction ops arbitrary: s)
    case Nil
    have "execute_parallel_operator s Nil
      = foldl (++) s (map (map_of ∘ effect_to_assignments) Nil)"
      using Nil.prems(1,2)
      unfolding execute_parallel_operator_def
      by presburger
    also have "… = s"
      by simp
    finally have "execute_parallel_operator s Nil = s"
      by blast
    moreover have "execute_serial_plan s Nil = s"
      by auto
    ultimately show ?case
      by simp
  next
    case (Cons a ops)
    ― ‹ NOTE Use the preceding lemmas to show that the premises hold for the sublist and use the IH
  to obtain the theorem for the sublist ops. ›
    have a: "is_operator_applicable_in s a"
      using are_all_operators_applicable_cons Cons.prems(1)
      by blast+
    let ?s' = "s ++ map_of (effect_to_assignments a)"
    {
      from Cons.prems
      have "are_all_operators_applicable ?s' ops"
        and "are_all_operator_effects_consistent ops"
        and "are_all_operators_non_interfering ops"
        using execute_parallel_plan_precondition_cons
        by blast+
      then have "execute_serial_plan ?s' ops
        = execute_parallel_operator ?s' ops"
        using Cons.IH
        by presburger
    }
    moreover from Cons.prems
    have "execute_parallel_operator s (Cons a ops)
      = execute_parallel_operator ?s' ops"
      using execute_parallel_operator_cons_equals_corollary
      unfolding execute_operator_def
      by simp
    moreover
    from a have "execute_serial_plan s (Cons a ops)
      = execute_serial_plan ?s' ops"
      unfolding execute_serial_plan_def execute_operator_def
        is_operator_applicable_in_def
      by fastforce
    ultimately show ?case
      by argo
  qed

lemma execute_serial_plan_split_i:
  assumes "are_all_operators_applicable s (op # π)"
    and "are_all_operators_non_interfering (op # π)"
  shows "are_all_operators_applicable (s ⪢ op) π"
  using assms
  proof (induction π arbitrary: s)
    case Nil
    then show ?case
      unfolding are_all_operators_applicable_def
      by simp
  next
    case (Cons op' π)
    let ?t = "s ⪢ op"
    {
      fix x
      assume "x ∈ set (op' # π)"
      moreover have "op ∈ set (op # op' # π)"
        by simp
      moreover have "¬are_operators_interfering op x"
        using Cons.prems(2) calculation(1)
        unfolding are_all_operators_non_interfering_def list_all_iff
        by fastforce
      moreover have "is_operator_applicable_in s op"
        using Cons.prems(1)
        unfolding are_all_operators_applicable_def list_all_iff
          is_operator_applicable_in_def
        by force
      moreover have "is_operator_applicable_in s x"
        using are_all_operators_applicable_cons(2)[OF Cons.prems(1)] calculation(1)
        unfolding are_all_operators_applicable_def list_all_iff
          is_operator_applicable_in_def
        by fast
      ultimately have "is_operator_applicable_in ?t x"
        using execute_parallel_plan_precondition_cons_i[of op x s]
        by (auto simp: execute_operator_def)
    }
    thus ?case
      using are_all_operators_applicable_cons(2)
      unfolding is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def
        are_all_operators_applicable_def list_all_iff
      by simp
  qed

― ‹ Show that plans $\pi$ can be split into separate executions of partial plans $\pi_1$ and
$\pi_2$ with $\pi = \pi_1 @ \pi_2$, if all operators in $\pi_1$ are applicable in the given state
$s$ and there is no interference between subsequent operators in $\pi_1$. This is the case because
non interference ensures that no precondition for any operator in $\pi_1$ is negated by the
execution of a preceding operator. Note that the non interference constraint excludes partial
plans where a precondition is first violated during execution but later restored which would also
allow splitting but does not meet the non interference constraint (which must hold for all
possible executing orders). ›
lemma execute_serial_plan_split:
  fixes s :: "('variable, bool) state"
  assumes "are_all_operators_applicable s π⇩1"
    and "are_all_operators_non_interfering π⇩1"
  shows "execute_serial_plan s (π⇩1 @ π⇩2)
    = execute_serial_plan (execute_serial_plan s π⇩1) π⇩2"
  using assms
  proof (induction π⇩1 arbitrary: s)
    case (Cons op π⇩1)
    let ?t = "s ⪢ op"
    {
      have "are_all_operators_applicable (s ⪢ op) π⇩1"
        using execute_serial_plan_split_i[OF Cons.prems(1, 2)].
      moreover have "are_all_operators_non_interfering π⇩1"
        using are_all_operators_non_interfering_tail[OF Cons.prems(2)].
      ultimately have "execute_serial_plan ?t (π⇩1 @ π⇩2) =
        execute_serial_plan (execute_serial_plan ?t π⇩1) π⇩2"
        using Cons.IH[of ?t]
        by blast
    }
    moreover have "STRIPS_Representation.is_operator_applicable_in s op"
      using Cons.prems(1)
      unfolding are_all_operators_applicable_def list_all_iff
      by fastforce
    ultimately show ?case
      unfolding execute_serial_plan_def
      by simp
  qed simp

(* TODO refactor *)
lemma embedding_lemma_i:
  fixes I :: "('variable, bool) state"
  assumes "is_operator_applicable_in I op"
    and "are_operator_effects_consistent op op"
  shows "I ⪢ op = execute_parallel_operator I [op]"
  proof -
    have "are_all_operators_applicable I [op]"
      using assms(1)
      unfolding are_all_operators_applicable_def list_all_iff is_operator_applicable_in_def
      by fastforce
    moreover have "are_all_operator_effects_consistent [op]"
      unfolding are_all_operator_effects_consistent_def list_all_iff
      using assms(2)
      by fastforce
    moreover have "are_all_operators_non_interfering [op]"
      by simp
    moreover have "I ⪢ op = execute_serial_plan I [op]"
      using assms(1)
      unfolding  is_operator_applicable_in_def
      by (simp add: assms(1) execute_operator_def)
    ultimately show ?thesis
      using execute_parallel_operator_equals_execute_sequential_strips_if
      by force
  qed

lemma execute_serial_plan_is_execute_parallel_plan_ii:
  fixes I :: "'variable strips_state"
  assumes "∀op ∈ set π. are_operator_effects_consistent op op"
    and "G ⊆⇩m execute_serial_plan I π"
  shows "G ⊆⇩m execute_parallel_plan I (embed π)"
  proof -
    show ?thesis
      using assms
      proof (induction π arbitrary: I)
        case (Cons op π)
        then show ?case
          proof (cases "is_operator_applicable_in I op")
            case True
            let ?J = "I ⪢ op"
              and ?J' = "execute_parallel_operator I [op]"
            {
              have "G ⊆⇩m execute_serial_plan ?J π"
                using Cons.prems(2) True
                unfolding is_operator_applicable_in_def
                by (simp add: True)
              hence "G ⊆⇩m execute_parallel_plan ?J (embed π)"
                using Cons.IH[of ?J] Cons.prems(1)
                by fastforce
            }
            moreover {
              have "are_all_operators_applicable I [op]"
                using True
                unfolding are_all_operators_applicable_def list_all_iff
                  is_operator_applicable_in_def
                by fastforce
              moreover have "are_all_operator_effects_consistent [op]"
                unfolding are_all_operator_effects_consistent_def list_all_iff
                using Cons.prems(1)
                by fastforce
              moreover have "?J = ?J'"
                using execute_parallel_operator_equals_execute_sequential_strips_if[OF
                    calculation(1, 2)] Cons.prems(1) True
                unfolding  is_operator_applicable_in_def
                by (simp add: True)
              ultimately have "execute_parallel_plan I (embed (op # π))
                = execute_parallel_plan ?J (embed π)"
                by fastforce
            }
            ultimately show ?thesis
              by presburger
          next
            case False
            then have "G ⊆⇩m I"
              using Cons.prems is_operator_applicable_in_def
              by simp
            moreover {
              have "¬are_all_operators_applicable I [op]"
                using False
                unfolding are_all_operators_applicable_def list_all_iff
                  is_operator_applicable_in_def
                by force
              hence "execute_parallel_plan I (embed (op # π)) = I"
                by simp
            }
            ultimately show ?thesis
              by presburger
          qed
      qed simp
  qed

lemma embedding_lemma_iii:
  fixes Π:: "'a strips_problem"
  assumes "∀op ∈ set π. op ∈ set ((Π)⇩𝒪)"
  shows "∀ops ∈ set (embed π). ∀op ∈ set ops. op ∈ set ((Π)⇩𝒪)"
  proof -
    (* TODO refactor *)
    have nb: "set (embed π) = { [op] | op. op ∈ set π }"
      by (induction π; force)
    {
      fix ops
      assume "ops ∈ set (embed π)"
      moreover obtain op where "op ∈ set π" and "ops = [op]"
        using nb calculation
        by blast
      ultimately have "∀op ∈ set ops. op ∈ set ((Π)⇩𝒪)"
        using assms(1)
        by simp
    }
    thus ?thesis..
  qed

text ‹ We show in the following theorem that---as mentioned---a serial solution \<^term>‹π› to a
STRIPS problem \<^term>‹Π› corresponds directly to a parallel solution obtained by embedding each operator
in \<^term>‹π› in a list (by use of function \<^term>‹embed›). The proof shows this by first
confirming that

    @{text[display, indent=4] "G ⊆⇩m execute_serial_plan ((Π)⇩I) π
    ⟹ G ⊆⇩m execute_serial_plan ((Π)⇩I) (embed π)"}

using lemma \isaname{execute_serial_plan_is_execute_parallel_plan_strip_ii}; and
moreover by showing that

    @{text[display, indent=4] "∀ops ∈ set (embed π). ∀op ∈ set ops. op ∈ (Π)⇩𝒪"}

meaning that under the given assumptions, all parallel operators of the embedded serial plan are
again operators in the operator set of the problem. ›
theorem  embedding_lemma:
  assumes "is_valid_problem_strips Π"
    and "is_serial_solution_for_problem Π π"
  shows "is_parallel_solution_for_problem Π (embed π)"
  proof  -
    (* TODO refactor ‹STRIPS_Representation› (characterization of valid operator).
  *)have nb⇩1: "∀op ∈ set π. op ∈ set ((Π)⇩𝒪)"
      using assms(2)
      unfolding is_serial_solution_for_problem_def list_all_iff ListMem_iff operators_of_def
      by blast
    (* TODO refactor lemma is_valid_operator_strips_then
  *)      {
      fix op
      assume "op ∈ set π"
      moreover have "op ∈ set ((Π)⇩𝒪)"
        using nb⇩1 calculation
        by fast
      moreover have "is_valid_operator_strips Π op"
        using assms(1) calculation(2)
        unfolding is_valid_problem_strips_def is_valid_problem_strips_def list_all_iff operators_of_def
        by meson
      moreover have "list_all (λv. ¬ListMem v (delete_effects_of op)) (add_effects_of op)"
        and "list_all (λv. ¬ListMem v (add_effects_of op)) (delete_effects_of op)"
        using calculation(3)
        unfolding is_valid_operator_strips_def
        by meson+
      moreover have "¬list_ex (λv. ListMem v (delete_effects_of op)) (add_effects_of op)"
        and "¬list_ex (λv. ListMem v (add_effects_of op)) (delete_effects_of op)"
        using calculation(4, 5) not_list_ex_equals_list_all_not
        by blast+
      moreover have "¬list_ex (λv. list_ex ((=) v) (delete_effects_of op)) (add_effects_of op)"
        and "¬list_ex (λv. list_ex ((=) v) (add_effects_of op)) (delete_effects_of op)"
        using calculation(6, 7)
        unfolding list_ex_iff ListMem_iff
        by blast+
      ultimately have "are_operator_effects_consistent op op"
        unfolding are_operator_effects_consistent_def Let_def
        by blast
    } note nb⇩2 = this
    moreover {
      have "(Π)⇩G ⊆⇩m execute_serial_plan ((Π)⇩I) π"
        using assms(2)
        unfolding is_serial_solution_for_problem_def
        by simp
      hence "(Π)⇩G ⊆⇩m execute_parallel_plan ((Π)⇩I) (embed π)"
        using execute_serial_plan_is_execute_parallel_plan_ii nb⇩2
        by blast
    }
    moreover have "∀ops ∈ set (embed π). ∀op ∈ set ops. op ∈ set ((Π)⇩𝒪)"
      using embedding_lemma_iii[OF nb⇩1].
    ultimately show ?thesis
      unfolding is_parallel_solution_for_problem_def goal_of_def
        initial_of_def operators_of_def list_all_iff ListMem_iff
      by blast
  qed

lemma flattening_lemma_i:
  fixes Π:: "'a strips_problem"
  assumes "∀ops ∈ set π. ∀op ∈ set ops. op ∈ set ((Π)⇩𝒪)"
  shows "∀op ∈ set (concat π). op ∈ set ((Π)⇩𝒪)"
  proof -
    {
      fix op
      assume "op ∈ set (concat π)"
      moreover have "op ∈ (⋃ops ∈ set π. set ops)"
        using calculation
        unfolding set_concat.
      then obtain ops where "ops ∈ set π" and "op ∈ set ops"
        using UN_iff
        by blast
      ultimately have "op ∈ set ((Π)⇩𝒪)"
        using assms
        by blast
    }
    thus ?thesis..
  qed

lemma flattening_lemma_ii:
  fixes I :: "'variable strips_state"
  assumes "∀ops ∈ set π. ∃op. ops = [op] ∧ is_valid_operator_strips Π op "
    and "G ⊆⇩m execute_parallel_plan I π"
  shows "G ⊆⇩m execute_serial_plan I (concat π)"
  proof -
    let ?π' = "concat π"
    (* TODO refactor lemma is_valid_operator_strips_then *)
    {
      fix op
      assume "is_valid_operator_strips Π op"
      moreover have "list_all (λv. ¬ListMem v (delete_effects_of op)) (add_effects_of op)"
        and "list_all (λv. ¬ListMem v (add_effects_of op)) (delete_effects_of op)"
        using calculation(1)
        unfolding is_valid_operator_strips_def
        by meson+
      moreover have "¬list_ex (λv. ListMem v (delete_effects_of op)) (add_effects_of op)"
        and "¬list_ex (λv. ListMem v (add_effects_of op)) (delete_effects_of op)"
        using calculation(2, 3) not_list_ex_equals_list_all_not
        by blast+
      moreover have "¬list_ex (λv. list_ex ((=) v) (delete_effects_of op)) (add_effects_of op)"
        and "¬list_ex (λv. list_ex ((=) v) (add_effects_of op)) (delete_effects_of op)"
        using calculation(4, 5)
        unfolding list_ex_iff ListMem_iff
        by blast+
      ultimately have "are_operator_effects_consistent op op"
        unfolding are_operator_effects_consistent_def Let_def
        by blast
    } note nb⇩1 = this
    show ?thesis
      using assms
      proof (induction π arbitrary: I)
        case (Cons ops π)
        obtain op where ops_is: "ops = [op]" and is_valid_op: "is_valid_operator_strips Π op"
          using Cons.prems(1)
          by fastforce
        show ?case
          proof (cases "are_all_operators_applicable I ops")
            case True
            let ?J = "execute_parallel_operator I [op]"
              and ?J' = "I ⪢ op"
            have nb⇩2: "is_operator_applicable_in I op"
              using True ops_is
              unfolding are_all_operators_applicable_def list_all_iff
                is_operator_applicable_in_def
              by simp
            have nb⇩3: "are_operator_effects_consistent op op"
              using nb⇩1[OF is_valid_op].
            {
              then have "are_all_operator_effects_consistent ops"
                unfolding are_all_operator_effects_consistent_def list_all_iff
                using ops_is
                by fastforce
              hence "G ⊆⇩m execute_parallel_plan ?J π"
                using Cons.prems(2) ops_is True
                by fastforce
            }
            moreover have "execute_serial_plan I (concat (ops # π))
              = execute_serial_plan ?J' (concat π)"
              using ops_is nb⇩2
              unfolding is_operator_applicable_in_def
              by (simp add: execute_operator_def nb⇩2)
            moreover have "?J = ?J'"
              unfolding execute_parallel_operator_def execute_operator_def comp_apply
              by fastforce
            ultimately show ?thesis
              using Cons.IH Cons.prems
              by force
          next
            case False
            moreover have "G ⊆⇩m I"
              using Cons.prems(2) calculation
              by force
            moreover {
              have "¬is_operator_applicable_in I op"
                using ops_is False
                unfolding are_all_operators_applicable_def list_all_iff
                  is_operator_applicable_in_def
                by fastforce
              hence "execute_serial_plan I (concat (ops # π)) = I"
                using ops_is is_operator_applicable_in_def
                by simp
            }
            ultimately show ?thesis
              by argo
          qed
      qed force
  qed

text ‹ The opposite direction is also easy to show if we can normalize the parallel plan to the
form of an embedded serial plan as shown below. ›

lemma flattening_lemma:
  assumes "is_valid_problem_strips Π"
    and "∀ops ∈ set π. ∃op. ops = [op]"
    and "is_parallel_solution_for_problem Π π"
  shows "is_serial_solution_for_problem Π (concat π)"
  proof  -
    let ?π' = "concat π"
    {
      have "∀ops ∈ set π. ∀op ∈ set ops. op ∈ set ((Π)⇩𝒪)"
        using assms(3)
        unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff
        by force
      hence "∀op ∈ set ?π'. op ∈ set ((Π)⇩𝒪)"
        using flattening_lemma_i
        by blast
    }
    moreover {
      {
        fix ops
        assume "ops ∈ set π"
        moreover obtain op where "ops = [op]"
          using assms(2) calculation
          by blast
        moreover have "op ∈ set ((Π)⇩𝒪)"
          using assms(3) calculation
          unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff
          by force
        moreover have "is_valid_operator_strips Π op"
          using assms(1) calculation(3)
          unfolding is_valid_problem_strips_def Let_def list_all_iff ListMem_iff
          by simp
        ultimately have "∃op. ops = [op] ∧ is_valid_operator_strips Π op"
          by blast
      }
      moreover have "(Π)⇩G ⊆⇩m execute_parallel_plan ((Π)⇩I) π"
        using assms(3)
        unfolding is_parallel_solution_for_problem_def
        by simp
      ultimately have "(Π)⇩G ⊆⇩m execute_serial_plan ((Π)⇩I) ?π'"
        using flattening_lemma_ii
        by blast
    }
    ultimately show "is_serial_solution_for_problem Π ?π'"
      unfolding is_serial_solution_for_problem_def list_all_iff ListMem_iff
      by simp
  qed


text ‹ Finally, we can obtain the important result that a parallel plan with a trace that
reaches the goal state of a given problem \<^term>‹Π›, and for which both the parallel operator execution
condition as well as non interference is assured at every point \<^term>‹k < length π›, the flattening of
the parallel plan \<^term>‹concat π› is a serial solution for the initial and goal state of the problem.
To wit, by lemma \ref{isathm:parallel-solution-trace-strips} we have

    @{text[display, indent=4] "(G ⊆⇩m execute_parallel_plan I π)
      = (G ⊆⇩m last (trace_parallel_plan_strips I π))"}

so the second assumption entails that \<^term>‹π› is a solution for the initial state and the goal state
of the problem. (which implicitely means that  \<^term>‹π› is a solution
for the inital state and goal state of the problem). The trace formulation is used in this case
because it allows us to write the---state dependent---applicability condition more succinctly. The
proof (shown below) is by structural induction on \<^term>‹π› with arbitrary initial state.›

(* TODO Demote to lemma; add theorem about problem solutions. Move text to theorem. *)
theorem  execute_parallel_plan_is_execute_sequential_plan_if:
  fixes I :: "('variable, bool) state"
  assumes "is_valid_problem Π"
    and "G ⊆⇩m last (trace_parallel_plan_strips I π)"
    and "∀k < length π.
      are_all_operators_applicable (trace_parallel_plan_strips I π ! k) (π ! k)
      ∧ are_all_operator_effects_consistent (π ! k)
      ∧ are_all_operators_non_interfering (π ! k)"
  shows "G ⊆⇩m execute_serial_plan I (concat π)"
  using assms
  proof (induction π arbitrary: I)
    case (Cons ops π)
    let ?ops' = "take (length ops) (concat (ops # π))"
    let ?J = "execute_parallel_operator I ops"
      and ?J' = "execute_serial_plan I ?ops'"
    {
      have "trace_parallel_plan_strips I π ! 0 = I" and "(ops # π) ! 0 = ops"
        unfolding trace_parallel_plan_strips_head_is_initial_state
        by simp+
      then have "are_all_operators_applicable I ops"
        and "are_all_operator_effects_consistent ops"
        and "are_all_operators_non_interfering ops"
        using Cons.prems(3)
        by auto+
      then have "trace_parallel_plan_strips I (ops # π)
        = I # trace_parallel_plan_strips ?J π"
        by fastforce
    } note nb = this
    {
      have "last (trace_parallel_plan_strips I (ops # π))
        = last (trace_parallel_plan_strips ?J π)"
        using trace_parallel_plan_strips_last_cons_then nb
        by metis
      hence "G ⊆⇩m last (trace_parallel_plan_strips ?J π)"
        using Cons.prems(2)
        by force
    }
    moreover {
      fix k
      assume "k < length π"
      moreover have "k + 1 < length (ops # π)"
        using calculation
        by force
      moreover have "π ! k = (ops # π) ! (k + 1)"
        by simp
      ultimately have "are_all_operators_applicable
        (trace_parallel_plan_strips ?J π ! k) (π ! k)"
        and "are_all_operator_effects_consistent (π ! k)"
        and "are_all_operators_non_interfering (π ! k)"
        using Cons.prems(3) nb
        by force+
    }
    ultimately have "G ⊆⇩m execute_serial_plan ?J (concat π)"
      using Cons.IH[OF Cons.prems(1), of ?J]
      by blast
    moreover {
      have "execute_serial_plan I (concat (ops # π))
        = execute_serial_plan ?J' (concat π)"
        using execute_serial_plan_split[of I ops] Cons.prems(3)
        by auto
      thm execute_parallel_operator_equals_execute_sequential_strips_if[of I]
      moreover have "?J = ?J'"
        using execute_parallel_operator_equals_execute_sequential_strips_if Cons.prems(3)
        by fastforce
      ultimately have "execute_serial_plan I (concat (ops # π))
        = execute_serial_plan ?J (concat π)"
        using execute_serial_plan_split[of I ops] Cons.prems(3)
        by argo
    }
    ultimately show ?case
      by argo
  qed force

subsection "Auxiliary lemmas about STRIPS"

lemma set_to_precondition_of_op_is[simp]: "set (to_precondition op)
  = { (v, True) | v. v ∈ set (precondition_of op) }"
  unfolding to_precondition_def STRIPS_Representation.to_precondition_def set_map
  by blast


end